DEFINITION aplus_gz_le()
TYPE =
       ∀k:nat
         .∀h:nat
           .∀n:nat
             .le h k
               →eq A (aplus gz (ASort h n) k) (ASort O (plus (minus k h) n))
BODY =
Show proof