include "nat/plus.ma".
-ntheorem foo: \forall x, y. ((λz. x + x = z + z) ?).
-##[ #x; #y; nnormalize; nauto.
\ No newline at end of file
+ntheorem foo:
+ ((λx.x + 0 = x) ?) →
+ ((λx,y.x + S y = S (x + y)) ? ?) →
+ ((λx,y.y + x = x + y) ? ?) →
+ ∀x. ((λz. x + x = z + S z) ?).
+##[ #H; #H1; #H2; #x; nnormalize in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file