---

Step * 1 of Lemma complete_nat_ind

.....assertion..... 
1. [P] : ℕ ⟶ ℙ
2. ∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])@i
3. i : ℕ@i
⊢ ∀n:ℕ. ∀i:ℕn.  P[i]
BY
{ (Thin (-1) THEN InductionOnNat THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}i.  P[j])  {}\mRightarrow{}  P[i])@i
3.  i  :  \mBbbN{}@i
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    P[i]


By

---

Latex:
(Thin  (-1)  THEN  InductionOnNat  THEN  Auto)

---

Home Index