---

Step * of Lemma fresh-cname_wf

No Annotations
∀[I:Cname List]. (fresh-cname(I) ∈ {x:Cname| ¬(x ∈ I)} )
BY
{ (Auto THEN (Assert [1 / I] ∈ {1...} List BY Auto)) }

1
1. I : Cname List
2. [1 / I] ∈ {1...} List
⊢ fresh-cname(I) ∈ {x:Cname| ¬(x ∈ I)} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:Cname  List].  (fresh-cname(I)  \mmember{}  \{x:Cname|  \mneg{}(x  \mmember{}  I)\}  )


By

---

Latex:
(Auto  THEN  (Assert  [1  /  I]  \mmember{}  \{1...\}  List  BY  Auto))

---

Home Index