...

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 9be9508e019ea712e3f0bba44eeb4b9b8b7b5ace..2368affe0fca9711d74ff0395518b28483f10a4b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -168,9 +168,7 @@ definition SUBSETS': carr3 (arrows3 CAT2 (category2_of_category1 REL) OA).
      [ apply (orelation_of_relation S T);
      | intros; apply (orelation_of_relation_preserves_equality S T a a' e); ]
   | apply orelation_of_relation_preserves_identity;
-  | simplify; intros;
-    apply (.= (orelation_of_relation_preserves_composition o1 o2 o4 f1 (f3∘f2)));
-    apply (#‡(orelation_of_relation_preserves_composition o2 o3 o4 f2 f3)); ]
+  | apply orelation_of_relation_preserves_composition; ]
 qed.
 
 theorem SUBSETS_faithful:
@@ -184,23 +182,26 @@ theorem SUBSETS_faithful:
   |*: cases Hletin1; cases x1; change in f3 with (eq1 ? x w); apply (. f3‡#); assumption;]
 qed.
 
-theorem SUBSETS_full: ∀S,T.∀f.∃g. map_arrows2 ?? SUBSETS' S T g = f.
+inductive exT2 (A:Type2) (P:A→CProp2) : CProp2 ≝
+  ex_introT2: ∀w:A. P w → exT2 A P.
+
+theorem SUBSETS_full: ∀S,T.∀f. exT2 ? (λg. map_arrows2 ?? SUBSETS' S T g = f).
  intros; exists;
   [ constructor 1; constructor 1;
-     [ apply (λx.λy. y ∈ f (singleton S x));
+     [ apply (λx:carr S.λy:carr T. y ∈ f (singleton S x));
      | intros; unfold FunClass_1_OF_carr2; lapply (.= e1‡#);
         [4: apply mem; |6: apply Hletin;|1,2,3,5: skip]
-       lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]
-     | whd; split; whd; intro; simplify; unfold map_arrows2; simplify;
+       lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]  
+     | whd; split; whd; intro; simplify; unfold map_arrows2; simplify; 
         [ split;
            [ change with (∀a1.(∀x. a1 ∈ f (singleton S x) → x ∈ a) → a1 ∈ f⎻* a);
            | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f (singleton S x) → x ∈ a)); ]
         | split;
-           [ change with (∀a1.(∃y. y ∈ f (singleton S a1) ∧ y ∈ a) → a1 ∈ f⎻ a);
-           | change with (∀a1.a1 ∈ f⎻ a → (∃y.y ∈ f (singleton S a1) ∧ y ∈ a)); ]
+           [ change with (∀a1.(∃y:carr T. y ∈ f (singleton S a1) ∧ y ∈ a) → a1 ∈ f⎻ a);
+           | change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f (singleton S a1) ∧ y ∈ a)); ]
         | split;
-           [ change with (∀a1.(∃x. a1 ∈ f (singleton S x) ∧ x ∈ a) → a1 ∈ f a);
-           | change with (∀a1.a1 ∈ f a → (∃x. a1 ∈ f (singleton S x) ∧ x ∈ a)); ]
+           [ change with (∀a1.(∃x:carr S. a1 ∈ f (singleton S x) ∧ x ∈ a) → a1 ∈ f a);
+           | change with (∀a1.a1 ∈ f a → (∃x:carr S. a1 ∈ f (singleton S x) ∧ x ∈ a)); ]
         | split;
            [ change with (∀a1.(∀y. y ∈ f (singleton S a1) → y ∈ a) → a1 ∈ f* a);
            | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f (singleton S a1) → y ∈ a)); ]]
@@ -243,4 +244,4 @@ theorem SUBSETS_full: ∀S,T.∀f.∃g. map_arrows2 ?? SUBSETS' S T g = f.
            [ intros 2; change in f3 with (eq1 ? a1 a2); change with (a2 ∈ f* a);
              apply (. f3^-1‡#); assumption;
            | assumption ]]]
-qed. 
+qed.
\ No newline at end of file