---

Step * of Lemma extd-nameset-nil

extd-nameset([]) ⊆r ℕ2
BY
{ D 0 }

1
.....subterm..... T:t
1:n
1. x : extd-nameset([])@i
⊢ x ∈ ℕ2

2
.....eq aux..... 
extd-nameset([]) ∈ Type

---

Latex:

---

Latex:
extd-nameset([])  \msubseteq{}r  \mBbbN{}2


By

---

Latex:
D  0

---

Home Index