From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 Jan 2009 22:13:10 +0000 (+0000)
Subject: universe inconsistency fixed
X-Git-Tag: make_still_working~4243
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5ab72ef7c6da38f9bc239e13f049521922987183;p=helm.git

universe inconsistency fixed
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index 7073900b1..bdadaf0fe 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -15,7 +15,7 @@
 include "o-basic_pairs.ma".
 include "o-basic_topologies.ma".
 
-
+alias symbol "eq" = "setoid1 eq".
 
 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
 definition o_basic_topology_of_o_basic_pair: BP → BTop.
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