---

Step * 1 of Lemma extd-nameset-nil

.....subterm..... T:t
1:n
1. x : extd-nameset([])@i
⊢ x ∈ ℕ2
BY
{ (Unfold `extd-nameset` -1 THEN (D_b_union (-1) THENA Auto)) }

1
1. a1 : nameset([])@i
⊢ a1 ∈ ℕ2

2
1. a1 : ℕ2@i
⊢ a1 ∈ ℕ2

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  x  :  extd-nameset([])@i
\mvdash{}  x  \mmember{}  \mBbbN{}2


By

---

Latex:
(Unfold  `extd-nameset`  -1  THEN  (D\_b\_union  (-1)  THENA  Auto))

---

Home Index