---

Step * of Lemma nat_ind

∀[P:ℕ ⟶ ℙ{k}]. (P[0] ⇒ (∀i:ℕ+. (P[i - 1] ⇒ P[i])) ⇒ {∀j:ℕ. P[j]})
BY
{ ((Unfold `guard` 0 THEN UnivCD) THENA Auto) }

1
1. [P] : ℕ ⟶ ℙ{k}
2. P[0]@k
3. ∀i:ℕ+. (P[i - 1] ⇒ P[i])@[k | i]
4. j : ℕ@i
⊢ P[j]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  -  1]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  \{\mforall{}j:\mBbbN{}.  P[j]\})


By

---

Latex:
((Unfold  `guard`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index