DEFINITION leqz_ind()
TYPE =
       ∀P:A→A→Prop
         .∀n:nat
             .∀n1:nat
               .∀n2:nat.∀n3:nat.(eq nat (plus n n3) (plus n1 n2))→(P (ASort n n2) (ASort n1 n3))
           →(∀a:A
                  .∀a1:A
                    .leqz a a1
                      →(P a a1)→∀a2:A.∀a3:A.(leqz a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
                →∀a:A.∀a1:A.(leqz a a1)→(P a a1))
BODY =
        assume P: A→A→Prop
        suppose H: 
           ∀n:nat
             .∀n1:nat
               .∀n2:nat.∀n3:nat.(eq nat (plus n n3) (plus n1 n2))→(P (ASort n n2) (ASort n1 n3))
        suppose H1: 
           ∀a:A
             .∀a1:A
               .leqz a a1
                 →(P a a1)→∀a2:A.∀a3:A.(leqz a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
          (aux) by well-founded reasoning we prove ∀a:A.∀a1:A.(leqz a a1)→(P a a1)
           assume a: A
           assume a1: A
           suppose H2: leqz a a1
             by cases on H2 we prove P a a1
                case leqz_sort n:nat n1:nat n2:nat n3:nat H3:eq nat (plus n n3) (plus n1 n2) ⇒
                   the thesis becomes P (ASort n n2) (ASort n1 n3)
                   by (H . . . . H3)
P (ASort n n2) (ASort n1 n3)
                case leqz_head a2:A a3:A H3:leqz a2 a3 a4:A a5:A H4:leqz a4 a5 ⇒
                   the thesis becomes P (AHead a2 a4) (AHead a3 a5)
                   (h1) by (aux . . H3) we proved P a2 a3
                   (h2) by (aux . . H4) we proved P a4 a5
                   by (H1 . . H3 h1 . . H4 h2)
P (AHead a2 a4) (AHead a3 a5)
             we proved P a a1
∀a:A.∀a1:A.(leqz a a1)→(P a a1)
          done
          consider aux
          we proved ∀a:A.∀a1:A.(leqz a a1)→(P a a1)
       we proved 
          ∀P:A→A→Prop
            .∀n:nat
                .∀n1:nat
                  .∀n2:nat.∀n3:nat.(eq nat (plus n n3) (plus n1 n2))→(P (ASort n n2) (ASort n1 n3))
              →(∀a:A
                     .∀a1:A
                       .leqz a a1
                         →(P a a1)→∀a2:A.∀a3:A.(leqz a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
                   →∀a:A.∀a1:A.(leqz a a1)→(P a a1))