DEFINITION aplus_asucc()
TYPE =
       ∀g:G.∀h:nat.∀a:A.(eq A (aplus g (asucc g a) h) (asucc g (aplus g a h)))
BODY =
Show proof