\ldots used here and there. Cool!

[helm.git] / helm / software / matita / nlibrary / sets / setoids.ma

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index ed2973d87af9170b0a910a747f42f64f343e8ce6..9d31b09439dc29f0b12eb9550140f9918f41ac3a 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -37,14 +37,14 @@ nrecord function_space (A,B: setoid): Type ≝
  }.
 
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
-(*
+
 ndefinition function_space_setoid: setoid → setoid → setoid.
  #A; #B; napply (mk_setoid ?????);
 ##[ napply (function_space A B);
 ##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a)));
 ##| nwhd; #x; #a;
     napply (f_ok ? ? x ? ? ?); (* QUI!! *)
-    unfold carr; unfold proofs; simplify;
+(*    unfold carr; unfold proofs; simplify;
     apply (refl A)
   | simplify;
     intros;