(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/plus.ma".
+set "baseuri" "cic:/matita/nat/plus".
include "logic/equality.ma".
include "nat/nat.ma".
qed.
theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m)
-\def injective_plus_l.
\ No newline at end of file
+\def injective_plus_l.