From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Mar 2010 18:14:54 +0000 (+0000)
Subject: Good definition found.
X-Git-Tag: make_still_working~2955
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c57405141d26ac2215a07b05d27a16a691dda50e;p=helm.git

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 9087304bd..046bcbf88 100644
--- 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