X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids.ma;h=e40dad6f6d20e4e3a1f7624b6f28b5d6056a6ef3;hb=456a157eba1428fd4ec02713e60ac2b653a0e0b0;hp=a7a5e74b0bbfa26f89b7e981a5d49da75e62d167;hpb=6f2f5039ef719f60ebcf24d7ee17c83eac6cc635;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index a7a5e74b0..e40dad6f6 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -103,10 +103,11 @@ ndefinition comp_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
-   R ≟ mk_unary_morphism ?? (composition ??? f g)
-        (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
+   R ≟ mk_unary_morphism o1 o3 
+        (composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g))
+        (prop1 o1 o3 (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
-     fun1 o1 o3 R ≡ (composition o1 o2 o3 f g).
+    fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g).
 
 ndefinition comp_binary_morphisms: 
   ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).