---

Step * of Lemma left_move_add_inr_lemma

∀x,H,G:Top.  (left-move(G ⊕ H;inr x ) ~ G ⊕ left-move(H;x))
BY
{ (Auto THEN (RW (AddrC [1;1] UnfoldTopAbC) 0 THEN RepUR ``left-move mkGame Wsup`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,H,G:Top.    (left-move(G  \moplus{}  H;inr  x  )  \msim{}  G  \moplus{}  left-move(H;x))


By

---

Latex:
(Auto  THEN  (RW  (AddrC  [1;1]  UnfoldTopAbC)  0  THEN  RepUR  ``left-move  mkGame  Wsup``  0)  THEN  Auto)

---

Home Index