DEFINITION A_ind()
TYPE =
       ∀P:A→Prop
         .∀n:nat.∀n1:nat.(P (ASort n n1))
           →(∀a:A.(P a)→∀a1:A.(P a1)→(P (AHead a a1)))→∀a:A.(P a)
BODY =
        assume P: A→Prop
        suppose H: ∀n:nat.∀n1:nat.(P (ASort n n1))
        suppose H1: ∀a:A.(P a)→∀a1:A.(P a1)→(P (AHead a a1))
          (aux) by well-founded reasoning we prove ∀a:A.(P a)
          assume a: A
             by cases on a we prove P a
                case ASort n:nat n1:nat ⇒
                   the thesis becomes P (ASort n n1)
                   by (H . .)
P (ASort n n1)
                case AHead a1:A a2:A ⇒
                   the thesis becomes P (AHead a1 a2)
                   (h1) by (aux .) we proved P a1
                   (h2) by (aux .) we proved P a2
                   by (H1 . h1 . h2)
P (AHead a1 a2)
             we proved P a
∀a:A.(P a)
          done
          consider aux
          we proved ∀a:A.(P a)
       we proved 
          ∀P:A→Prop
            .∀n:nat.∀n1:nat.(P (ASort n n1))
              →(∀a:A.(P a)→∀a1:A.(P a1)→(P (AHead a a1)))→∀a:A.(P a)