---

Step * of Lemma fib_wf

∀[n:ℕ]. (fib(n) ∈ ℕ)
BY
{ ((D 0 THENA Auto) THEN (OnVar `n' CompNatInd THENA Auto)) }

1
1. n : ℕ
2. ∀n:ℕn. (fib(n) ∈ ℕ)
⊢ fib(n) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (fib(n)  \mmember{}  \mBbbN{})


By

---

Latex:
((D  0  THENA  Auto)  THEN  (OnVar  `n'  CompNatInd  THENA  Auto))

---

Home Index