(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL/ZEq/setoid".
+
include "NPlus/fun.ma".
include "ZEq/defs.ma".
theorem zeq_refl: \forall z. z = z.
intros. elim z. clear z.
- lapply (nplus_total t t1). decompose.
+ lapply (nplus_total a b). decompose.
autobatch.
qed.