\forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq
nat (next_plus g (next_plus g n h1) h2) (next_plus g n (plus h1 h2))))))
\def
\forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq
nat (next_plus g (next_plus g n h1) h2) (next_plus g n (plus h1 h2))))))
\def