DEFINITION leq_ind()
TYPE =
       ∀g:G
         .∀P:A→A→Prop
           .∀n:nat
               .∀n1:nat
                 .∀n2:nat
                   .∀n3:nat
                     .∀n4:nat
                       .eq A (aplus g (ASort n n2) n4) (aplus g (ASort n1 n3) n4)
                         →P (ASort n n2) (ASort n1 n3)
             →(∀a:A
                    .∀a1:A
                      .leq g a a1
                        →(P a a1)→∀a2:A.∀a3:A.(leq g a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
                  →∀a:A.∀a1:A.(leq g a a1)→(P a a1))
BODY =
        assume g: G
        assume P: A→A→Prop
        suppose H: 
           ∀n:nat
             .∀n1:nat
               .∀n2:nat
                 .∀n3:nat
                   .∀n4:nat
                     .eq A (aplus g (ASort n n2) n4) (aplus g (ASort n1 n3) n4)
                       →P (ASort n n2) (ASort n1 n3)
        suppose H1: 
           ∀a:A
             .∀a1:A
               .leq g a a1
                 →(P a a1)→∀a2:A.∀a3:A.(leq g a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
          (aux) by well-founded reasoning we prove ∀a:A.∀a1:A.(leq g a a1)→(P a a1)
           assume a: A
           assume a1: A
           suppose H2: leq g a a1
             by cases on H2 we prove P a a1
                case leq_sort n:nat n1:nat n2:nat n3:nat n4:nat H3:eq A (aplus g (ASort n n2) n4) (aplus g (ASort n1 n3) n4) ⇒
                   the thesis becomes P (ASort n n2) (ASort n1 n3)
                   by (H . . . . . H3)
P (ASort n n2) (ASort n1 n3)
                case leq_head a2:A a3:A H3:leq g a2 a3 a4:A a5:A H4:leq g 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.(leq g a a1)→(P a a1)
          done
          consider aux
          we proved ∀a:A.∀a1:A.(leq g a a1)→(P a a1)
       we proved 
          ∀g:G
            .∀P:A→A→Prop
              .∀n:nat
                  .∀n1:nat
                    .∀n2:nat
                      .∀n3:nat
                        .∀n4:nat
                          .eq A (aplus g (ASort n n2) n4) (aplus g (ASort n1 n3) n4)
                            →P (ASort n n2) (ASort n1 n3)
                →(∀a:A
                       .∀a1:A
                         .leq g a a1
                           →(P a a1)→∀a2:A.∀a3:A.(leq g a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
                     →∀a:A.∀a1:A.(leq g a a1)→(P a a1))