X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=56a8c4120b802e3b65dc73f14417820c22d58855;hb=e189bde1e0a562e8689ff41d55d392431609e749;hp=15da20a1132aae02cb7df0a5b457096402649eb2;hpb=aa5f71baeba0299c0d29be01798f7a1ad13656f9;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 15da20a11..56a8c4120 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -109,6 +109,24 @@ theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a 
        assumption]]
 qed.
 
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+  (∀a:A. a ∈ U → P a) →
+   (∀a:A.∀V:Ω \sup 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.
+
 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  intros;
  cases H;