More work.

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index cb720ffb484bef6b08ed01df81b50ad3ce6876ff..257139aef9c495de557c3285a756dabd0ee97032 100644 (file)
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -47,27 +47,20 @@ for @{ 'covers $a $b }.
 interpretation "covers" 'covers a U = (covers _ U a).
 interpretation "coversl" 'covers A U = (coversl _ U A).
 
-axiom covers_elim:
- ∀A:axiom_set.∀U: 2 \sup A.∀P:A → CProp.
-  ∀H1:∀a:A. a ∈ U → P a.
-   ∀H2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
-    ∀a:A.∀p:a ◃ U.P a.
-(*
 definition covers_elim ≝
- λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
-  λH1:∀a:A. a ∈ U → a ∈ P.
-   λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P.
-    let rec aux (a:A) (p:a ◃ U) : a ∈ P ≝
-     match p return λaa.λ_.aa ∈ P with
+ λA:axiom_set.λU: 2 \sup A.λP:A → CProp.
+  λH1:∀a:A. a ∈ U → P a.
+   λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
+    let rec aux (a:A) (p:a ◃ U) on p : P a ≝
+     match p return λaa.λ_:aa ◃ U.P aa with
       [ refl a q ⇒ H1 a q
       | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
       ]
-    and auxl (V: 2 \sup A) (q: V ◃ U) : ∀b. b ∈ V → b ∈ P ≝
-     match q return λVV.λ_.∀b. b ∈ VV → b ∈ P with
+    and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → P b ≝
+     match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → P b with
       [ iter VV f ⇒ λb.λr. aux b (f b r) ]
     in
-     aux.
-*) 
+     aux. 
 
 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
  mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
@@ -111,4 +104,12 @@ theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a 
      [ assumption
      | constructor 1;
        assumption]]
-qed.
\ No newline at end of file
+qed.
+
+theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
+ intros;
+ cases H;
+ cases H1;
+ assumption.
+qed.
+