---

Step * of Lemma left_move_add_inl_lemma

∀x,H,G:Top.  (left-move(G ⊕ H;inl x) ~ left-move(G;x) ⊕ H)
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;inl  x)  \msim{}  left-move(G;x)  \moplus{}  H)


By

---

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

---

Home Index