---

Step * of Lemma all-nsub2

∀[P:ℕ2 ⟶ ℙ]. (∀x:ℕ2. P[x] ⇐⇒ P[0] ∧ P[1])
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. [P] : ℕ2 ⟶ ℙ
2. ∀x:ℕ2. P[x]@i
⊢ P[0] ∧ P[1]

2
1. [P] : ℕ2 ⟶ ℙ
2. P[0] ∧ P[1]@i
⊢ ∀x:ℕ2. P[x]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}2  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}x:\mBbbN{}2.  P[x]  \mLeftarrow{}{}\mRightarrow{}  P[0]  \mwedge{}  P[1])


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index