DEFINITION leq_ind()
TYPE =
       ∀g:G
         .∀P:A→A→Prop
           .∀n:nat
               .∀n1:nat
                 .∀n2:nat
                   .∀n3:nat
                     .∀n4:nat
                       .eq A (aplus g (ASort n n2) n4) (aplus g (ASort n1 n3) n4)
                         →P (ASort n n2) (ASort n1 n3)
             →(∀a:A
                    .∀a1:A
                      .leq g a a1
                        →(P a a1)→∀a2:A.∀a3:A.(leq g a2 a3)→(P a2 a3)→(P (AHead a a2) (AHead a1 a3))
                  →∀a:A.∀a1:A.(leq g a a1)→(P a a1))
BODY =
Show proof