---

Step * 5 of Lemma assert-isname

.....wf..... 
1. L : Cname List
2. z : extd-nameset(L)
⊢ z ∈ nameset(L) ∈ Type
BY
{ (GenConcl ⌜z = b ∈ Base⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  Cname  List
2.  z  :  extd-nameset(L)
\mvdash{}  z  \mmember{}  nameset(L)  \mmember{}  Type


By

---

Latex:
(GenConcl  \mkleeneopen{}z  =  b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index