---

Step * of Lemma same-binding-trans

No Annotations
∀[vs,ws,us:varname() List]. ∀[v,w,u:varname()].
  ((↑same-binding(vs;ws;v;w)) ⇒ (↑same-binding(ws;us;w;u)) ⇒ (↑same-binding(vs;us;v;u)))
BY
{ (RepeatFor 3 (InductionOnList)
   THEN Unfold `same-binding` 0
   THEN Reduce 0
   THEN Auto
   THEN All (RW assert_pushdownC)
   THEN Auto
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN RenameVar `a' (-3)
   THEN RenameVar `b' (-1)
   THEN (BoolCase ⌜eq_var(u;a)⌝⋅ THENA Auto)
   THEN BoolCase ⌜eq_var(u1;w)⌝⋅
   THEN Auto
   THEN RW assert_pushdownC (-1)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RepeatFor  3  (InductionOnList)
  THEN  Unfold  `same-binding`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  All  (RW  assert\_pushdownC)
  THEN  Auto
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  RenameVar  `a'  (-3)
  THEN  RenameVar  `b'  (-1)
  THEN  (BoolCase  \mkleeneopen{}eq\_var(u;a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  BoolCase  \mkleeneopen{}eq\_var(u1;w)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)

---

Home Index