DEFINITION aplus_inj()
TYPE =
       ∀g:G.∀h1:nat.∀h2:nat.∀a:A.(eq A (aplus g a h1) (aplus g a h2))→(eq nat h1 h2)
BODY =
Show proof