T s tlist tlt iso
C r flt app
lift cnt drop clear getl clen cimp
lift1 drop1
subst0 subst1 subst csubst0 csubst1 fsubst0 
G next_plus
sty0 sty1
A asucc aplus leq llt aprem ex0 
pr0 wcpr0 pr1 pr2 pr3 
csubv arity csuba
nf2 sn3 sc3 csubc ex2
pc1 pc3
ty3 csubt wf3 ex1