---

Step * of Lemma sg-change-init_wf

∀[g:SimpleGame]. ∀[j:Pos(g)].  (g@j ∈ SimpleGame)
BY
{ (Intros THEN Unfold `sg-change-init` 0 THEN Unhide) }

1
1. g : SimpleGame
2. j : Pos(g)
⊢ let p,i,l1,l2 = g 
  in <{y:p| sg-reachable(g;j;y)} , j, l1, l2>   ∈ SimpleGame

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[j:Pos(g)].    (g@j  \mmember{}  SimpleGame)


By

---

Latex:
(Intros  THEN  Unfold  `sg-change-init`  0  THEN  Unhide)

---

Home Index