---

Step * of Lemma Game-minus_wf

∀[G:Game]. (-(G) ∈ Game)
BY
{ ((D 0 THENA Auto) THEN Unfold `Game` 1) }

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

---

Latex:

---

Latex:
\mforall{}[G:Game].  (-(G)  \mmember{}  Game)


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `Game`  1)

---

Home Index