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 =
Show proof