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