---

Step * of Lemma maybe_new_var_wf

No Annotations
∀[v:varname()]. ∀[vs:varname() List].  (maybe_new_var(v;vs) ∈ varname())
BY
{ (Intros THEN Unhide THEN (D 1 THEN Try (D 1)) THEN RepUR ``maybe_new_var`` 0 THEN Unfold `varname` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[v:varname()].  \mforall{}[vs:varname()  List].    (maybe\_new\_var(v;vs)  \mmember{}  varname())


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (D  1  THEN  Try  (D  1))
  THEN  RepUR  ``maybe\_new\_var``  0
  THEN  Unfold  `varname`  0
  THEN  Auto)

---

Home Index