---

Step * of Lemma maybe-new-local_wf

∀[me,s:Name]. ∀[avoid:Name List].  (maybe-new-local(me;s;avoid) ∈ Name)
BY
{ (UnivCD THENA Auto)
THEN Unfold `maybe-new-local` 0
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[me,s:Name].  \mforall{}[avoid:Name  List].    (maybe-new-local(me;s;avoid)  \mmember{}  Name)


By

---

Latex:
(UnivCD  THENA  Auto)
THEN  Unfold  `maybe-new-local`  0
THEN  Auto

---

Home Index