DEFINITION leqz_ind()
TYPE =
       P:AAProp
         .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