1) stuff moved from categories.ma to setoids*.ma

[helm.git] / helm / software / matita / nlibrary / overlap / o-algebra.ma

diff --git a/helm/software/matita/nlibrary/overlap/o-algebra.ma b/helm/software/matita/nlibrary/overlap/o-algebra.ma
index ce922a38aa05c8dd272655d9663b8bf137fc143b..227ef04517d4d65f92121d066d3240606928e7d6 100644 (file)
--- a/helm/software/matita/nlibrary/overlap/o-algebra.ma
+++ b/helm/software/matita/nlibrary/overlap/o-algebra.ma
@@ -308,34 +308,29 @@ unification hint 0 ≔ P, Q, r;
 (* ------------------------ *) ⊢
   fun11 … R r ≡ or_f_minus_star P Q r.
 
-(*CSC:
 ndefinition ORelation_composition : ∀P,Q,R. 
   binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
 #P; #Q; #R; @
 [ #F; #G; @
-  [ napply (G ∘ F);
-  | apply rule (G⎻* ∘ F⎻* );
-  | apply (F* ∘ G* );
-  | apply (F⎻ ∘ G⎻);
-  | intros; 
-    change with ((G (F p) ≤ q) = (p ≤ (F* (G* q))));
-    apply (.= (or_prop1 :?));
-    apply (or_prop1 :?);
-  | intros;
-    change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q))));
-    apply (.= (or_prop2 :?));
-    apply or_prop2 ; 
-  | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q))));
-    apply (.= (or_prop3 :?));
-    apply or_prop3;
+  [ napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*)
+  | napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)
+  | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
+  | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
+  | #p; #q; nnormalize;
+    napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
+    napply (or_prop1 …)
+  | #p; #q; nnormalize;
+    napply (.= (or_prop2 … F …));
+    napply or_prop2
+  | #p; #q; nnormalize;
+    napply (.= (or_prop3 … G …));
+    napply or_prop3
   ]
-| intros; split; simplify; 
-   [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
-   |1: apply ((†e)‡(†e1));
-   |2,4: apply ((†e1)‡(†e));]]
-qed.
+##| #a;#a';#b;#b';#e;#e1;#x;nnormalize;napply (.= †(e x));napply e1]
+nqed.
 
-definition OA : category2.
+(*
+ndefinition OA : category2.
 split;
 [ apply (OAlgebra);
 | intros; apply (ORelation_setoid o o1);