---

Step * of Lemma fib-exists

∀n:ℕ. (∃m:{ℕ| (m = fib(n) ∈ ℕ)})
BY
{ (Auto THEN With ⌜fib(n)⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}m:\{\mBbbN{}|  (m  =  fib(n))\})


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}fib(n)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index