X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;h=69e0958744de4f83c3257f88ad3b8e4ac78ef8fa;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=fa615c8e4d74600903d6e1cdd845eb3524ad6f3f;hpb=fd52068e75c3ea1e67b2066ac9f7e2a862148a18;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index fa615c8e4..69e095874 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -104,14 +104,11 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:unary_morphism1 o2 o3,g:unary_morphism
  (* -------------------------------------------------------------------- *) ⊢
                               fun11 ?? R ≡ (composition1 … f g).
                               
-(*
-ndefinition comp_binary_morphisms:
+ndefinition comp1_binary_morphisms:
  ∀o1,o2,o3.
-  binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2)
-   (unary_morphism1_setoid1 o1 o3).
-#o1; #o2; #o3; @
+  unary_morphism1 (unary_morphism1_setoid1 o2 o3)
+   (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)).
+#o1; #o2; #o3; napply mk_binary_morphism1
  [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
- | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize;
-   napply (.= †(eb x)); napply ea.
-nqed.
-*)
+ | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
+nqed.
\ No newline at end of file