+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.
+