---

Step * of Lemma same-binding_wf

No Annotations
∀[vs,ws:varname() List]. ∀[v,w:varname()].  (same-binding(vs;ws;v;w) ∈ 𝔹)
BY
{ (RepeatFor 2 (InductionOnList) THEN Auto THEN (Unfold `same-binding` 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[vs,ws:varname()  List].  \mforall{}[v,w:varname()].    (same-binding(vs;ws;v;w)  \mmember{}  \mBbbB{})


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Auto  THEN  (Unfold  `same-binding`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index