INDUCTIVE DEFINITION leqz () [ ]
OF ARITY A→A→Prop
BUILT FROM:
     leqz_sort: ∀h1:nat
                         .∀h2:nat
                           .∀n1:nat
                             .∀n2:nat.(eq nat (plus h1 n2) (plus h2 n1))→(leqz (ASort h1 n1) (ASort h2 n2))
   | leqz_head: ∀a1:A.∀a2:A.(leqz a1 a2)→∀a3:A.∀a4:A.(leqz a3 a4)→(leqz (AHead a1 a3) (AHead a2 a4))