DEFINITION leq_asucc()
TYPE =
       ∀g:G.∀a:A.(ex A λa0:A.leq g a (asucc g a0))
BODY =
        assume g: G
        assume a: A
          we proceed by induction on a to prove ex A λa1:A.leq g a (asucc g a1)
             case ASort : n:nat n0:nat ⇒
                the thesis becomes ex A λa0:A.leq g (ASort n n0) (asucc g a0)
                   by (leq_refl . .)
                   we proved leq g (ASort n n0) (ASort n n0)
                   that is equivalent to leq g (ASort n n0) (asucc g (ASort (S n) n0))
                   by (ex_intro . . . previous)
ex A λa0:A.leq g (ASort n n0) (asucc g a0)
             case AHead : a0:A a1:A ⇒
                the thesis becomes ex A λa2:A.leq g (AHead a0 a1) (asucc g a2)
                () by induction hypothesis we know ex A λa1:A.leq g a0 (asucc g a1)
                (H0) by induction hypothesis we know ex A λa2:A.leq g a1 (asucc g a2)
                   (H1) consider H0
                   we proceed by induction on H1 to prove ex A λa2:A.leq g (AHead a0 a1) (asucc g a2)
                      case ex_intro : x:A H2:leq g a1 (asucc g x) ⇒
                         the thesis becomes ex A λa2:A.leq g (AHead a0 a1) (asucc g a2)
                            by (leq_refl . .)
                            we proved leq g a0 a0
                            by (leq_head . . . previous . . H2)
                            we proved leq g (AHead a0 a1) (AHead a0 (asucc g x))
                            that is equivalent to leq g (AHead a0 a1) (asucc g (AHead a0 x))
                            by (ex_intro . . . previous)
ex A λa2:A.leq g (AHead a0 a1) (asucc g a2)
ex A λa2:A.leq g (AHead a0 a1) (asucc g a2)
          we proved ex A λa1:A.leq g a (asucc g a1)
       we proved ∀g:G.∀a:A.(ex A λa1:A.leq g a (asucc g a1))