DEFINITION aplus_asort_simpl()
TYPE =
       ∀g:G
         .∀h:nat
           .∀k:nat
             .∀n:nat
               .eq
                 A
                 aplus g (ASort k n) h
                 ASort (minus k h) (next_plus g n (minus h k))
BODY =
Show proof