---

Step * of Lemma Game-add_wf

∀[G,H:Game].  (G ⊕ H ∈ Game)
BY
{ (Auto THEN MoveToConcl (-1) THEN Unfold `Game` 1) }

1
1. G : W(GameA{i:l}();p.GameB(p))
⊢ ∀H:Game. (G ⊕ H ∈ Game)

---

Latex:

---

Latex:
\mforall{}[G,H:Game].    (G  \moplus{}  H  \mmember{}  Game)


By

---

Latex:
(Auto  THEN  MoveToConcl  (-1)  THEN  Unfold  `Game`  1)

---

Home Index