---

Step * 1 1 of Lemma extd-nameset-nil


1. a1 : nameset([])@i
⊢ a1 ∈ ℕ2
BY
{ (D -1 THEN RW ListC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  a1  :  nameset([])@i
\mvdash{}  a1  \mmember{}  \mBbbN{}2


By

---

Latex:
(D  -1  THEN  RW  ListC  (-1)  THEN  Auto)

---

Home Index