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