X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations_to_o-algebra.ma;h=7f2710640ddf83d38385b9b15380644ac33ee8bc;hb=0080faad4e730c227b6bbb2549407b23703b477a;hp=9be9508e019ea712e3f0bba44eeb4b9b8b7b5ace;hpb=6b71ae123d3e412d43872b8b7965b7013a970d05;p=helm.git

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 9be9508e0..7f2710640 100644
--- 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
@@ -184,23 +184,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 +246,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