X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FZah%2Fsetoid.ma;h=681d6338503d4809e341064ca05e73c35f3e8859;hb=b54b2b352753b1c784d06118fc689c1ee9f9feaf;hp=e30b5a205723b3ae8cbad46098bdb2d1edc99989;hpb=40fe102ced39ae6b315c03327ab248dfca473ee4;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma b/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
index e30b5a205..681d63385 100644
--- a/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
+++ b/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
@@ -21,7 +21,7 @@ theorem nplus_total: \forall p,q. \exists r. p + q == r.
  intros 2. elim q; clear q;
  decompose; auto.
 qed.
-
+(*
 theorem zeq_intro: \forall z1,z2. 
                    (\forall n.((\fst z1) + (\snd z2) == n) \to ((\fst z2) + (\snd z1) == n)) \to
                    (\forall n.((\fst z2) + (\snd z1) == n) \to ((\fst z1) + (\snd z2) == n)) \to
@@ -36,7 +36,7 @@ qed.
 theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
  unfold ZEq. intros. lapply linear (H n). auto.
 qed.
-(*
+*)(*
 theorem zeq_trans: \forall z1,z2. z1 = z2 \to 
                    \forall z3. z2 = z3 \to z1 = z3.
  unfold ZEq. intros.