INDUCTIVE DEFINITION leq () [ :G ]
OF ARITY A→A→Prop
BUILT FROM:
     leq_sort: ∀h1:nat
                       .∀h2:nat
                         .∀n1:nat
                           .∀n2:nat
                             .∀k:nat
                               .eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)
                                 →leq g (ASort h1 n1) (ASort h2 n2)
   | leq_head: ∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.∀a4:A.(leq g a3 a4)→(leq g (AHead a1 a3) (AHead a2 a4))