Compatibility finished.

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index d828f8c4ea2c7445127f43d2727c0e2915315c1e..ca544b598d190874ba01f6c13fd49db946651883 100644 (file)
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -53,8 +53,8 @@ with coversl : (2 \sup A) → CProp ≝
 notation "hvbox(a break ◃ b)" non associative with precedence 45
 for @{ 'covers $a $b }.
 
-interpretation "covers" 'covers a U = (covers _ U a).
 interpretation "coversl" 'covers A U = (coversl _ U A).
+interpretation "covers" 'covers a U = (covers _ U a).
 
 definition covers_elim ≝
  λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
@@ -73,10 +73,12 @@ definition covers_elim ≝
 
 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
  mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
+definition fishl ≝ λA:axiom_set.λU:2 \sup A.λV:2 \sup A. ∃a. a ∈ V ∧ fish ? U a.
 
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
 for @{ 'fish $a $b }.
 
+interpretation "fishl" 'fish A U = (fishl _ U A).
 interpretation "fish" 'fish a U = (fish _ U a).
 
 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
@@ -104,7 +106,7 @@ qed.
 
 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  intros;
- apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); intros;
+ apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); simplify; intros;
   [ cases H1 in H2;
     intro;
     apply H2;
@@ -123,11 +125,26 @@ theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
 qed.
 
 theorem cotransitivity:
- ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b. b ⋉ U → b ∈ V) → a ⋉ V.
+ ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
  intros;
  apply (fish_rec ?? (mk_powerset A (λa.a ⋉ U)) ??? H); simplify; intros;
   [ apply H1;
     assumption
   | cases H2 in j; clear H2; cases H3; clear H3;
     assumption]
+qed.
+
+theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
+ intros;
+ generalize in match H; clear H; generalize in match V; clear V;
+ apply (covers_elim ?? (mk_powerset A (λa.∀p:2 \sup A.a ⋉ p → U ⋉ p)) ??? H1);
+ clear H1; simplify; intros;
+  [ exists [apply a1]
+    split;
+    assumption
+  | cases H2 in j H H1; clear H2 a1; intros;
+    cases H; clear H;
+    cases (H4 i); clear H4; cases H; clear H;
+    apply (H2 w); clear H2;
+    assumption]
 qed.
\ No newline at end of file