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