\forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (h1: nat).(\forall
(h2: nat).((eq A (aplus g a1 h1) (aplus g a2 h2)) \to (\forall (h: nat).(eq A
(aplus g a1 (plus h h1)) (aplus g a2 (plus h h2)))))))))
\forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (h1: nat).(\forall
(h2: nat).((eq A (aplus g a1 h1) (aplus g a2 h2)) \to (\forall (h: nat).(eq A
(aplus g a1 (plus h h1)) (aplus g a2 (plus h h2)))))))))