AMBDA-TYPES: some improvements. subst now fully exploited

[helm.git] / matita / contribs / RELATIONAL / Zah / setoid.ma

diff --git a/matita/contribs/RELATIONAL/Zah/setoid.ma b/matita/contribs/RELATIONAL/Zah/setoid.ma
index e30b5a205723b3ae8cbad46098bdb2d1edc99989..681d6338503d4809e341064ca05e73c35f3e8859 100644 (file)
--- a/matita/contribs/RELATIONAL/Zah/setoid.ma
+++ b/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.