DEFINITION aplus_ahead_simpl()
TYPE =
       ∀g:G.∀h:nat.∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) h) (AHead a1 (aplus g a2 h)))
BODY =
Show proof