---

Step * 1 of Lemma Game-add_wf


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

1
1. a : GameA{i:l}()
2. f : GameB(a) ⟶ W(GameA{i:l}();a.GameB(a))
3. ∀b:GameB(a). ∀H:Game.  (f b ⊕ H ∈ Game)
⊢ ∀H:Game. (Wsup(a;f) ⊕ H ∈ Game)

---

Latex:

---

Latex:

1.  G  :  W(GameA\{i:l\}();p.GameB(p))
\mvdash{}  \mforall{}H:Game.  (G  \moplus{}  H  \mmember{}  Game)


By

---

Latex:
WElim  1

---

Home Index