+nlemma ftcoreflexivity: ∀A: Ax_pro.∀F.∀a:A. a ⋉ F → a ∈ F.
+ #A; #F; #a; #H; ncases H; //.
+nqed.
+
+nlemma ftcoleqinfinity:
+ ∀A: Ax_pro.∀F.∀a:A. a ⋉ F →
+ ∀b. (a ≤ b → ∀i. (∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ x ⋉ F)).
+ #A; #F; #a; #H; ncases H; /2/.
+nqed.
+
+nlemma ftcoleqleft:
+ ∀A: Ax_pro.∀F.∀a:A. a ⋉ F →
+ (∀b. a ≤ b → b ⋉ F).
+ #A; #F; #a; #H; ncases H; /2/.
+nqed.
+
+alias symbol "I" (instance 7) = "I".
+alias symbol "I" (instance 18) = "I".
+alias symbol "I" (instance 18) = "I".
+alias symbol "I" (instance 18) = "I".
+nlet corec ftfish_coind
+ (A: Ax_pro) (F: Ω^A) (P: A → CProp[0])
+ (Hcorefl: ∀a. P a → a ∈ F)
+ (Hcoleqleft: ∀a. P a → ∀b. a ≤ b → P b)
+ (Hcoleqinfinity: ∀a. P a → ∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ P x)
+: ∀a:A. P a → a ⋉ F ≝ ?.
+ #a; #H; @
+ [ /2/
+ | #b; #H; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); /2/
+ | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3;
+ @ x; @; //; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); //]
+nqed.
+
+(*CSC: non serve manco questo (vedi sotto) *)
+nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
+ #A; //.
+nqed.
+