---

Step * of Lemma complete-nat-induction

∀[P:ℕ ⟶ ℙ]. ((∀n:ℕ. ((∀m:ℕn. P[m]) ⇒ P[n])) ⇒ (∀n:ℕ. P[n]))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN All (RepUR ``all implies``) THEN RenameVar `g' (-1)) }

1
1. [P] : ℕ ⟶ ℙ
2. g : n:ℕ ⟶ (m:ℕn ⟶ P[m]) ⟶ P[n]@i
⊢ n:ℕ ⟶ P[n]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}n:\mBbbN{}.  ((\mforall{}m:\mBbbN{}n.  P[m])  {}\mRightarrow{}  P[n]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  P[n]))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  All  (RepUR  ``all  implies``)  THEN  RenameVar  `g'  (-1))

---

Home Index