From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Aug 2009 15:35:24 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3517
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cde41460616634f77c2c11b585400dcc613b88f1;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 29e1f1af3..8e05ca6f4 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -1,3 +1,4 @@
+
 include "logic/connectives.ma".
 
 nrecord powerset (X : Type[0]) : Type[1] ≝ { char : X → CProp[0] }.
@@ -73,41 +74,23 @@ nlet corec fish_rec (A:axiom_set) (U: Ω^A)
 ##]
 nqed.
 
-STOP
-
-theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
- intros;
- apply refl;
- assumption.
-qed.
-
-theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
- intros;
- apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
-  [ cases H1 in H2; apply H2;
-  | apply infinity;
-     [ assumption
-     | constructor 1;
-       assumption]]
-qed.
-
-theorem covers_elim2:
- ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers".
+ntheorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω^A.∀P: A → CProp[0].
   (∀a:A. a ∈ U → P a) →
-   (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+   (∀a:A.∀V:Ω^A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
      ∀a:A. a ◃ U → P a.
- intros;
- change with (a ∈ {a | P a});
- apply (covers_elim ?????? H2);
-  [ intros 2; simplify; apply H; assumption
-  | intros;
-    simplify in H4 ⊢ %;
-    apply H1;
-     [ apply (C ? a1 j);
-     | autobatch; 
-     | assumption;
-     | assumption]]
-qed.
+#A; #U; #P; #H1; #H2; #a; #aU; nelim aU;
+##[ #b; #H; napply H1; napply H;
+##| #b; #i; #CaiU; #H; napply H2; 
+    ##[ napply (C ? b i);
+    ##| napply cinfinity; ##[ napply i ] nwhd; #y; #H3; napply creflexivity; ##]
+    nassumption; 
+##]
+nqed.
+
+STOP
 
 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  intros;