---

Step * 1 of Lemma fresh-cname-not-member


1. [I] : Cname List
⊢ ¬(fresh-cname(I) ∈ nameset(I))
BY
{ D 0 }

1
1. [I] : Cname List
2. fresh-cname(I) ∈ nameset(I)
⊢ False

2
.....wf..... 
1. I : Cname List
⊢ fresh-cname(I) ∈ nameset(I) ∈ Type

---

Latex:

---

Latex:

1.  [I]  :  Cname  List
\mvdash{}  \mneg{}(fresh-cname(I)  \mmember{}  nameset(I))


By

---

Latex:
D  0

---

Home Index