+ | false ⇒
+*)
+
+include "topology/igft.ma".
+include "datatypes/pairs.ma".
+include "datatypes/sums.ma".
+
+nrecord pre_order (A: Type[0]) : Type[1] ≝
+ { pre_r :2> A → A → CProp[0];
+ pre_sym: reflexive … pre_r;
+ pre_trans: transitive … pre_r
+ }.
+
+nrecord Ax_pro : Type[1] ≝
+ { AAx :> Ax;
+ Aleq: pre_order AAx
+ }.
+
+interpretation "Ax_pro leq" 'leq x y = (pre_r ? (Aleq ?) x y).
+
+(*CSC: per auto per sotto, ma non sembra aiutare *)
+nlemma And_elim1: ∀A,B. A ∧ B → A.
+ #A; #B; *; //.
+nqed.
+
+nlemma And_elim2: ∀A,B. A ∧ B → B.
+ #A; #B; *; //.
+nqed.
+(*CSC: /fine per auto per sotto *)
+
+ndefinition Rax : Ax_pro.
+ @
+ [ @ (Q × Q)
+ [ #p; napply (unit + sigma … (λc. fst … p < fst … c ∧ fst … c < snd … c ∧ snd … c < snd … p))
+ | #c; *
+ [ #_; napply {c' | fst … c < fst … c' ∧ snd … c' < snd … c}
+ | *; #c'; #_; napply {d' | fst … d' = fst … c ∧ snd … d' = fst … c'
+ ∨ fst … d' = snd … c' ∧ snd … d' = snd … c } ]##]
+##| @ (λc,d. fst … d ≤ fst … c ∧ snd … c ≤ snd … d)
+ [ /2/
+ | nnormalize; #z; #x; #y; *; #H1; #H2; *; /3/; (*CSC: perche' non va? *) ##]
+nqed.
+
+ndefinition downarrow: ∀S:Ax_pro. Ω \sup S → Ω \sup S ≝
+ λS:Ax_pro.λU:Ω ^S.{a | ∃b:S. b ∈ U ∧ a ≤ b}.
+
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
+
+ndefinition fintersects: ∀S:Ax_pro. Ω \sup S → Ω \sup S → Ω \sup S ≝
+ λS.λU,V. ↓U ∩ ↓V.
+
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
+
+ndefinition singleton ≝ λA.λa:A.{b | b=a}.
+
+interpretation "singleton" 'singl a = (singleton ? a).
+
+ninductive ftcover (A : Ax_pro) (U : Ω^A) : A → CProp[0] ≝
+| ftreflexivity : ∀a. a ∈ U → ftcover A U a
+| ftleqinfinity : ∀a,b. a ≤ b → ∀i. (∀x. x ∈ 𝐂 b i ↓ (singleton … a) → ftcover A U x) → ftcover A U a
+| ftleqleft : ∀a,b. a ≤ b → ftcover A U b → ftcover A U a.
+
+interpretation "ftcovers" 'covers a U = (ftcover ? U a).
+
+ntheorem ftinfinity: ∀A: Ax_pro. ∀U: Ω^A. ∀a. ∀i. (∀x. x ∈ 𝐂 a i → x ◃ U) → a ◃ U.
+ #A; #U; #a; #i; #H;
+ napply (ftleqinfinity … a … i); //;
+ #x; *; *; #b; *; #H1; #H2; #H3; napply (ftleqleft … b); //;
+ napply H; napply H1 (*CSC: auto non va! *).
+nqed.
+
+ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
+| ftfish : ∀a.
+ a ∈ F →
+ (∀b. a ≤ b → ftfish A F b) →
+ (∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) →
+ ftfish A F a.
+
+interpretation "fish" 'fish a U = (ftfish ? U a).
+
+alias symbol "I" (instance 6) = "I".
+ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
+ #A; #F; #a; #H; ncases H; #b; #_; #_; #H2; #i; ncases (H2 … i); //;
+ #x; *; *; *; #y; *; #K2; #K3; #_; #K5; @y; @ K2; ncases K5 in K3; /2/.
+nqed.
\ No newline at end of file