From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 2 Feb 2009 09:10:54 +0000 (+0000)
Subject: Hmmm, going too low.
X-Git-Tag: make_still_working~4215
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=982eb9392e7fd9ee26a4ebf593244e8125ed7853;p=helm.git

Hmmm, going too low.
We need a more abstract proof (see Theorem 5.15, page 157 old book).
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 92e9e975d..72c5fe02d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -38,15 +38,23 @@ letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
  | constructor 1;
     [2: constructor 1; constructor 1;
       [ intros (x y); apply (y ∈ f (singleton ? x));
-      | intros; unfold FunClass_1_OF_Ocontinuous_relation;
+      | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
         unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
         apply rule #; ]
     |1: constructor 1; constructor 1;
       [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
-      | intros; unfold FunClass_1_OF_Ocontinuous_relation;
+      | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
         unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
         apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
-    | whd; simplify; intros; split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
+    | whd; simplify; intros; simplify;
+      whd in ⊢ (? % %); simplify in ⊢ (? % %);
+      lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
+       [ whd in Hletin; simplify in Hletin; cases Hletin; clear Hletin;
+         lapply (s y); clear s;
+whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
+whd in Hletin; simplify in Hletin;
+         lapply (s1 y); clear s1;      
+     split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
       cases f1; clear f1; cases x1; clear x1;
        [
        | exists;