---

Step * of Lemma fresh-cname-not-member

∀[I:Cname List]. (¬(fresh-cname(I) ∈ nameset(I)))
BY
{ (Intro THENA Auto) }

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

---

Latex:

---

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


By

---

Latex:
(Intro  THENA  Auto)

---

Home Index