...

[helm.git] / helm / software / matita / library / formal_topology / relations_to_o-algebra.ma

diff --git a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
index 01c06f02046a97a57df349dc2eddd626c100d1d9..bc5153d5db66532004203625260f99767955eea9 100644 (file)
--- a/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
+++ b/helm/software/matita/library/formal_topology/relations_to_o-algebra.ma
@@ -51,15 +51,13 @@ qed.
 definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
 coercion powerset_of_POW'.
 
-definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x.
-
 definition orelation_of_relation: ∀o1,o2:REL. o1 ⇒_\r1 o2 → (POW' o1) ⇒_\o2 (POW' o2).
  intros;
  constructor 1;
   [ apply rule c;
-  | apply rule ((foo ?? c)⎻* ); 
-  | apply rule ((foo ?? c)* );
-  | apply rule ((foo ?? c)⎻);
+  | apply rule (c⎻* ); 
+  | apply rule (c* );
+  | apply rule (c⎻);
   | intros; split; intro;
      [ intros 2; intros 2; apply (f y); exists[apply a] split; assumption;
      | intros 2; change with (a ∈ q); cases f1; cases x; clear f1 x; 
@@ -82,7 +80,7 @@ lemma orelation_of_relation_preserves_equality:
  change in e with (t =_2 t'); unfold image_coercion; apply (†e);
 qed.
 
-lemma minus_image_id : ∀o:REL.(foo ?? (id1 REL o))⎻ =_1 (id2 SET1 Ω^o).
+lemma minus_image_id : ∀o:REL.((id1 REL o))⎻ =_1 (id2 SET1 Ω^o).
 unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intros;
 [ cases e; cases x; change with (a1 ∈ a); change in f with (a1 =_1 w); 
   apply (. f‡#); assumption;
@@ -90,7 +88,7 @@ unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intro
   change with (a1 =_1 a1); apply refl1;]
 qed.
 
-lemma star_image_id : ∀o:REL.  (foo ?? (id1 REL o))* =_1 (id2 SET1 Ω^o).
+lemma star_image_id : ∀o:REL.  ((id1 REL o))* =_1 (id2 SET1 Ω^o).
 unfold foo; intro o; intro; unfold star_image; simplify; split; simplify; intros;
 [ change with (a1 ∈ a); apply f; change with (a1 =_1 a1); apply rule refl1;
 | change in f1 with (a1 =_1 y); apply (. f1^-1‡#); apply f;]
@@ -190,9 +188,6 @@ theorem POW_full: full2 ?? POW.
         [4: apply mem; |6: apply Hletin;|1,2,3,5: skip]
        lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]  
      | (split; intro; split; simplify);
-     (*
-     whd; split; whd; intro; simplify; unfold map_arrows2; simplify; 
-        [ split;*)
            [ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a);
            | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a)); 
            | alias symbol "and" (instance 4) = "and_morphism".