---

Step * of Lemma comp_nat_ind_a

∀[P:ℕ ⟶ ℙ{k}]. ((∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])) ⇒ {∀i:ℕ. P[i]})
BY
{ ((Unfold `guard` 0 THEN RepD) THENA Auto) }

1
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ P[i]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}].  ((\mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  \{\mforall{}i:\mBbbN{}.  P[i]\})


By

---

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

---

Home Index