X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;h=90be6bc94be18f5758c7ce8b8fb5ee8c2d63c5a4;hb=68b4f2490c12139c03760b39895619e63b0f38c9;hp=068334183dc698ebb9cb3dea09ed1e7942a87c28;hpb=2c486bbea1d6ffb072d0ff83f9df129b7860f3e1;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 068334183..90be6bc94 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -91,7 +91,7 @@ nqed.
 unification hint 0 ≔ S, T ;
    R ≟ (unary_morphism1_setoid1 S T)
 (* --------------------------------- *) ⊢
-   carr1 R ≡ S ⇒_1 T.
+   carr1 R ≡ unary_morphism1 S T.
    
 notation "l ╪_1 r" with precedence 89 for @{'prop2_x1 $l $r }.
 interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r).
@@ -120,10 +120,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 ??? (fun11 ?? f) (fun11 ?? g))
         (prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun11 ?? R ≡ (composition1 ??? f g).
+       fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g).
                               
 ndefinition comp1_binary_morphisms:
  ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).