(VAR a s t u )
(RULES 
        sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) -> sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))
        sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) -> sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
        sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) -> sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))
        sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) -> sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
        sortSu(circ(sortSu(s), sortSu(id))) -> sortSu(s)
        sortSu(circ(sortSu(id), sortSu(s))) -> sortSu(s)
        sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) -> sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
        te(subst(te(a), sortSu(id))) -> te(a)
        te(msubst(te(a), sortSu(id))) -> te(a)
        te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) -> te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
        
)