DEFINITION asucc_gen_sort()
TYPE =
       ∀g:G
         .∀h:nat
           .∀n:nat
             .∀a:A
               .eq A (ASort h n) (asucc g a)
                 →ex_2 nat nat λh0:nat.λn0:nat.eq A a (ASort h0 n0)
BODY =
        assume g: G
        assume h: nat
        assume n: nat
        assume a: A
          we proceed by induction on a to prove 
             eq A (ASort h n) (asucc g a)
               →ex_2 nat nat λh0:nat.λn0:nat.eq A a (ASort h0 n0)
             case ASort : n0:nat n1:nat ⇒
                the thesis becomes 
                ∀H:eq A (ASort h n) (asucc g (ASort n0 n1))
                  .ex_2 nat nat λh0:nat.λn2:nat.eq A (ASort n0 n1) (ASort h0 n2)
                   suppose H: eq A (ASort h n) (asucc g (ASort n0 n1))
                      by (refl_equal . .)
                      we proved eq A (ASort n0 n1) (ASort n0 n1)
                      by (ex_2_intro . . . . . previous)
                      we proved ex_2 nat nat λh0:nat.λn2:nat.eq A (ASort n0 n1) (ASort h0 n2)

                      ∀H:eq A (ASort h n) (asucc g (ASort n0 n1))
                        .ex_2 nat nat λh0:nat.λn2:nat.eq A (ASort n0 n1) (ASort h0 n2)
             case AHead : a0:A a1:A ⇒
                the thesis becomes 
                ∀H1:eq A (ASort h n) (asucc g (AHead a0 a1))
                  .ex_2 nat nat λh0:nat.λn0:nat.eq A (AHead a0 a1) (ASort h0 n0)
                () by induction hypothesis we know 
                   eq A (ASort h n) (asucc g a0)
                     →ex_2 nat nat λh0:nat.λn0:nat.eq A a0 (ASort h0 n0)
                () by induction hypothesis we know 
                   eq A (ASort h n) (asucc g a1)
                     →ex_2 nat nat λh0:nat.λn0:nat.eq A a1 (ASort h0 n0)
                   suppose H1: eq A (ASort h n) (asucc g (AHead a0 a1))
                      (H2) 
                         we proceed by induction on H1 to prove <λ:A.Prop> CASE asucc g (AHead a0 a1) OF ASort  ⇒True | AHead  ⇒False
                            case refl_equal : ⇒
                               the thesis becomes <λ:A.Prop> CASE ASort h n OF ASort  ⇒True | AHead  ⇒False
                                  consider I
                                  we proved True
<λ:A.Prop> CASE ASort h n OF ASort  ⇒True | AHead  ⇒False
<λ:A.Prop> CASE asucc g (AHead a0 a1) OF ASort  ⇒True | AHead  ⇒False
                      end of H2
                      consider H2
                      we proved <λ:A.Prop> CASE asucc g (AHead a0 a1) OF ASort  ⇒True | AHead  ⇒False
                      that is equivalent to False
                      we proceed by induction on the previous result to prove ex_2 nat nat λh0:nat.λn0:nat.eq A (AHead a0 a1) (ASort h0 n0)
                      we proved ex_2 nat nat λh0:nat.λn0:nat.eq A (AHead a0 a1) (ASort h0 n0)

                      ∀H1:eq A (ASort h n) (asucc g (AHead a0 a1))
                        .ex_2 nat nat λh0:nat.λn0:nat.eq A (AHead a0 a1) (ASort h0 n0)
          we proved 
             eq A (ASort h n) (asucc g a)
               →ex_2 nat nat λh0:nat.λn0:nat.eq A a (ASort h0 n0)
       we proved 
          ∀g:G
            .∀h:nat
              .∀n:nat
                .∀a:A
                  .eq A (ASort h n) (asucc g a)
                    →ex_2 nat nat λh0:nat.λn0:nat.eq A a (ASort h0 n0)