---

Step * of Lemma assert-isname

∀[L:Cname List]. ∀[z:extd-nameset(L)].  uiff(↑isname(z);z ∈ nameset(L))
BY
{ (Intros THEN RepeatFor 2 (D 0)) }

1
1. L : Cname List
2. z : extd-nameset(L)
3. ↑isname(z)
⊢ z ∈ nameset(L)

2
.....wf..... 
1. L : Cname List
2. z : extd-nameset(L)
⊢ ↑isname(z) ∈ ℙ

3
1. L : Cname List
2. z : extd-nameset(L)
3. z ∈ nameset(L)
⊢ ↑isname(z)

4
.....wf..... 
1. L : Cname List
2. z : extd-nameset(L)
3. z ∈ nameset(L)
4. ↑isname(z)
⊢ isname(z) ∈ 𝔹

5
.....wf..... 
1. L : Cname List
2. z : extd-nameset(L)
⊢ z ∈ nameset(L) ∈ Type

---

Latex:

---

Latex:
\mforall{}[L:Cname  List].  \mforall{}[z:extd-nameset(L)].    uiff(\muparrow{}isname(z);z  \mmember{}  nameset(L))


By

---

Latex:
(Intros  THEN  RepeatFor  2  (D  0))

---

Home Index