The new coercion from SET to Type0 with higher priority really helps a lot:

[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 781514e0757cfdbd2e33811ac1ba9f0c3d1c2210..e661fbfd082333a36cfb52a27b0517f3c42c33d8 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
@@ -30,26 +30,18 @@ definition SUBSETS: objs1 SET → OAlgebra.
   | intros; whd; split; assumption
   | intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption]
   | intros; cases f; exists [apply w] assumption
-  | intros; intros 2; apply (f ? f1 i);
-  | intros; intros 2; apply f;
-    (* senza questa change, universe inconsistency *)
-    whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
-    exists; [apply i] assumption;
+  | intros; split; [ intros 4; apply (f ? f1 i); | intros 3; intro; apply (f i ? f1); ]
+  | intros; split;
+     [ intros 4; apply f; exists; [apply i] assumption;
+     | intros 3; intros; cases f1; apply (f w a x); ]
   | intros 3; cases f;
   | intros 3; constructor 1;
   | intros; cases f; exists; [apply w]
      [ assumption
      | whd; intros; cases i; simplify; assumption]
   | intros; split; intro;
-     [ cases f; cases x1;
-       (* senza questa change, universe inconsistency *)
-       change in ⊢ (? ? (λ_:%.?)) with (carr I);
-       exists [apply w1] exists [apply w] assumption;
-     | cases e; cases x; exists; [apply w1]
-        [ assumption
-        | (* senza questa change, universe inconsistency *)
-          whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
-          exists; [apply w] assumption]]
+     [ cases f; cases x1; exists [apply w1] exists [apply w] assumption;
+     | cases e; cases x; exists; [apply w1] [ assumption | exists; [apply w] assumption]]
   | intros; intros 2; cases (f (singleton ? a) ?);
      [ exists; [apply a] [assumption | change with (a = a); apply refl1;]
      | change in x1 with (a = w); change with (mem A a q); apply (. (x1‡#));
@@ -129,15 +121,15 @@ lemma orelation_of_relation_preserves_identity:
   | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
     change in f1 with (x = a1); apply (. f1‡#); apply f;
   | alias symbol "and" = "and_morphism".
-    change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
+    change with ((∃y:o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
     intro; cases e; clear e; cases x; clear x; change in f with (a1=w);
     apply (. f‡#); apply f1;
-  | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
+  | change with (a1 ∈ a → ∃y:o1.a1 ♮(id1 REL o1) y ∧ y∈a);
     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
-  | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
+  | change with ((∃x:o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
     intro; cases e; clear e; cases x; clear x; change in f with (w=a1);
     apply (. f^-1‡#); apply f1;
-  | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
+  | change with (a1 ∈ a → ∃x:o1.x ♮(id1 REL o1) a1∧x∈a);
     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
   | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros;
     apply (f a1); change with (a1 = a1); apply refl1;