Some more painful work.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index a84fc24770ac859b40040b56a3ecdaf826d5c8ca..063e5988f0dec33ac678aba3ee3addb506fbdf8b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -99,7 +99,7 @@ interpretation "o-algebra leq" 'leq a b = (fun21 ___ (oa_leq _) a b).
 
 notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
 for @{ 'overlap $a $b}.
-interpretation "o-algebra overlap" 'overlap a b = (fun22 ___ (oa_overlap _) a b).
+interpretation "o-algebra overlap" 'overlap a b = (fun21 ___ (oa_overlap _) a b).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
 non associative with precedence 50 for @{ 'oa_meet $p }.
@@ -148,8 +148,8 @@ interpretation "o-algebra binary meet" 'oa_meet_bin a b =
   (fun21 ___ (binary_meet _) a b).
 
 lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
-intros;  lapply (oa_overlap_preservers_meet_ O p q f);
-lapply (prop1 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
+intros;  lapply (oa_overlap_preserves_meet_ O p q f);
+lapply (prop21 O O CPROP (oa_overlap O) p p ? (p ∧ q) # ?);
 [3: apply (if ?? (Hletin1)); apply Hletin;|skip] apply refl1;
 qed.
 
@@ -166,15 +166,20 @@ notation > "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
 
 interpretation "o-algebra join" 'oa_join f = 
-  (fun_1 __ (oa_join __) f).
+  (fun12 __ (oa_join __) f).
 interpretation "o-algebra join with explicit function" 'oa_join_mk f = 
-  (fun_1 __ (oa_join __) (mk_unary_morphism _ _ f _)).
+  (fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)).
+
+definition hint5: OAlgebra → objs2 SET1.
+ intro; apply (oa_P o);
+qed.
+coercion hint5.
 
 record ORelation (P,Q : OAlgebra) : Type ≝ {
-  or_f_ : arrows1 SET P Q;
-  or_f_minus_star_ : arrows1 SET P Q;
-  or_f_star_ : arrows1 SET Q P;
-  or_f_minus_ : arrows1 SET Q P;
+  or_f_ : P ⇒ Q;
+  or_f_minus_star_ : P ⇒ Q;
+  or_f_star_ : Q ⇒ P;
+  or_f_minus_ : Q ⇒ P;
   or_prop1_ : ∀p,q. (or_f_ p ≤ q) = (p ≤ or_f_star_ q);
   or_prop2_ : ∀p,q. (or_f_minus_ p ≤ q) = (p ≤ or_f_minus_star_ q);
   or_prop3_ : ∀p,q. (or_f_ p >< q) = (p >< or_f_minus_ q)
@@ -188,19 +193,19 @@ constructor 1;
 | constructor 1;
    (* tenere solo una uguaglianza e usare la proposizione 9.9 per
       le altre (unicita' degli aggiunti e del simmetrico) *)
-   [ apply (λp,q. And4 (eq1 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) 
-             (eq1 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q)) 
-             (eq1 ? (or_f_ ?? p) (or_f_ ?? q)) 
-             (eq1 ? (or_f_star_ ?? p) (or_f_star_ ?? q))); 
-   | whd; simplify; intros; repeat split; intros; apply refl1;
+   [ apply (λp,q. And4 (eq2 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q)) 
+             (eq2 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q)) 
+             (eq2 ? (or_f_ ?? p) (or_f_ ?? q)) 
+             (eq2 ? (or_f_star_ ?? p) (or_f_star_ ?? q))); 
+   | whd; simplify; intros; repeat split; intros; apply refl2;
    | whd; simplify; intros; cases H; clear H; split; 
-     intro a; apply sym; generalize in match a;assumption;
+     intro a; apply sym1; generalize in match a;assumption;
    | whd; simplify; intros; cases H; cases H1; clear H H1; split; intro a;
-     [ apply (.= (H2 a)); apply H6;
-     | apply (.= (H3 a)); apply H7;
-     | apply (.= (H4 a)); apply H8;
-     | apply (.= (H5 a)); apply H9;]]]
-qed.  
+     [ apply (.= (e a)); apply e4;
+     | apply (.= (e1 a)); apply e5;
+     | apply (.= (e2 a)); apply e6;
+     | apply (.= (e3 a)); apply e7;]]]
+qed.
 
 definition or_f_minus_star: ∀P,Q:OAlgebra.ORelation_setoid P Q ⇒ arrows1 SET P Q.
  intros; constructor 1;