---

Step * of Lemma primrec-induction

∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀n:ℕ. (P[n] ⇒ P[n + 1])) ⇒ (∀n:ℕ. P[n]))
BY
{ xxx(Auto THEN RenameVar `b' 2 THEN RenameVar `f' 3 ⋅)xxx }

1
1. [P] : ℕ ⟶ ℙ
2. b : P[0]
3. f : ∀n:ℕ. (P[n] ⇒ P[n + 1])
4. n : ℕ
⊢ P[n]

---

Latex:

---

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


By

---

Latex:
xxx(Auto  THEN  RenameVar  `b'  2  THEN  RenameVar  `f'  3  \mcdot{})xxx

---

Home Index