X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;fp=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;h=48b7d3fccc7709c6996014ec1ccf27aa82bb5776;hb=90ff94e74ceed0954b8599bff55d5c84f15c1b9f;hp=4ab57d568860ad1c4b505323f909eda3cbd39573;hpb=d86eefac7dff521eb2589b6f2dcb8a1b361be186;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 4ab57d568..48b7d3fcc 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -27,10 +27,21 @@ unification hint 0 ≔ R : setoid1;
 (* ---------------------------------------- *) ⊢ 
    setoid1 ≡ force2 ? MR lock.
 
+notation < "[\setoid1\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid1 $x}.
+interpretation "mk_setoid1" 'mk_setoid1 x = (mk_setoid1 x ?).
+
+(* da capire se mettere come coercion *)
 ndefinition setoid1_of_setoid: setoid → setoid1.
  #s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…);
 nqed.
 
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
+unification hint 0 ≔ A,x,y
+(*-----------------------------------------------*) ⊢
+   eq_rel ? (eq0 A) x y ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) x y.
+(* XXX capire come mai questa hint non funziona se porto su (setoid1_of_setoid A) *)
+
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
 
@@ -102,10 +113,10 @@ ndefinition comp1_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
-   R ≟ (mk_unary_morphism1 ?? (composition1 … f g)
+   R ≟ (mk_unary_morphism1 ?? (composition1 ??? f g)
         (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun11 ?? R ≡ (composition1 … f g).
+                              fun11 ?? R ≡ (composition1 ??? f g).
                               
 ndefinition comp1_binary_morphisms:
  ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).