Record projections are now defined as fixpoints in order to block

[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 40982a660438b3479e40d5502aba581041d2ec47..1a2ff09788820c3f9b7e374472ae1b0838f3562c 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -24,7 +24,7 @@ nrecord setoid : Type[1] ≝
  }.
 
 ndefinition proofs: CProp → setoid.
-#P; napply (mk_setoid …);
+#P; napply mk_setoid;
 ##[ napply P;
 ##| #x; #y; napply True;
 ##|##*: nwhd; nrepeat (#_); napply I;
@@ -39,25 +39,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 …);
+ #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;
-    apply (refl A)
-  | simplify;
-    intros;
-    unfold carr; unfold proofs; simplify;
-    apply (sym B);
-    apply (f a)
-  | simplify;
-    intros;
-    unfold carr; unfold proofs; simplify;
-    apply (trans B ? (y a));
-    [ apply (f a)
-    | apply (f1 a)]]
-qed.
+##| nnormalize; #x; #a; napply (f_ok … x); napply refl
+  | nnormalize; #x; #y; #H; #a; napply sym; napply H
+  | nnormalize; #z; #x; #y; #H1; #H2; #a;
+    napply trans; ##[##2: napply H1 | ##skip | napply H2]##] 
+nqed.
 
 nrecord isomorphism (A,B: setoid): Type ≝
  { map1:> function_space_setoid A B;