---

Step * 1 2 1 2 of Lemma decidable__nameset

.....wf..... 
1. L : Cname List
2. a : Cname
3. ¬(a ∈ L)
⊢ a ∈ nameset(L) ∈ Type
BY
{ (GenConcl ⌜a = x ∈ Base⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  Cname  List
2.  a  :  Cname
3.  \mneg{}(a  \mmember{}  L)
\mvdash{}  a  \mmember{}  nameset(L)  \mmember{}  Type


By

---

Latex:
(GenConcl  \mkleeneopen{}a  =  x\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index