DEFINITION leq_gen_sort1()
TYPE =
       ∀g:G
         .∀h1:nat
           .∀n1:nat
             .∀a2:A
               .leq g (ASort h1 n1) a2
                 →(ex2_3
                      nat
                      nat
                      nat
                      λn2:nat.λh2:nat.λk:nat.eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)
                      λn2:nat.λh2:nat.λ:nat.eq A a2 (ASort h2 n2))
BODY =
Show proof