...

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 29e1f1af31995ddc7f1a17158b3ee6c07fcd8d8d..8e05ca6f45b2e9aa1f93ef7d25b06fe5193ae64d 100644 (file)
--- 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;