qed.
theorem associative_plus : associative nat plus.
-simplify.intros.elim x.
+unfold associative.intros.elim x.
simplify.reflexivity.
simplify.apply eq_f.assumption.
qed.
theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
intro.simplify.intros.
-apply injective_plus_r m.
+apply (injective_plus_r m).
rewrite < sym_plus.
-rewrite < sym_plus y.
+rewrite < (sym_plus y).
assumption.
qed.