X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN%2Falgebra%2FSetoids.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN%2Falgebra%2FSetoids.ma;h=6b7bf781ddfc429aff3a745393d48bed6b793a1a;hb=67a2dc4999d7f47e57bf6ac2f6dc285e304e1737;hp=4fcb5a23be061042d8a70235f4dbb6692ced0da5;hpb=33e397c66c8ab7ff1adbffa6e3b2d152dbecad26;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN/algebra/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/Setoids.ma
index 4fcb5a23b..6b7bf781d 100644
--- a/helm/software/matita/contribs/CoRN/algebra/Setoids.ma
+++ b/helm/software/matita/contribs/CoRN/algebra/Setoids.ma
@@ -1227,11 +1227,6 @@ qed.
 
 
 
-axiom proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
- (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
- \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
-
-(*
 lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
  (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
  \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
@@ -1253,9 +1248,9 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-auto.
+auto new.
 qed.
-*)
+
 (*
 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
 *)