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