DEFINITION asucc()
TYPE =
       G→A→A
BODY =
FIXasucc{
         asucc:G→A→A
         :=λg:G
           .λl:A
             .<λa:A.A>
               CASE l OF
                 ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g n) | S h⇒ASort h n
               | AHead a1 a2⇒AHead a1 (asucc g a2)
         }