Good definition found.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 9087304bdda0c7b30d99627deb990f9d3991abc3..046bcbf88d8ec37c0fd6bc91e2b41f4d3c2d2a1b 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -169,16 +169,14 @@ nqed.
 ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
 | ftfish : ∀a.
     a ∈ F →
-    (*(∀i:𝐈 a .∃b. b ∈ 𝐂  a i ∧ ftfish A F b) →*)
     (∀b. a ≤ b → ftfish A F b) →
-    (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftcover A F x) →
+    (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) →
     ftfish A F a.
 
-ntheorem 
-
-interpretation "fish" 'fish a U = (fish ? U 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; *; #b; #H; #H1; #i; @ a; @; //;
- ncases H;  
\ No newline at end of file
+ #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