---

Step * of Lemma sg-init-change-init

∀[g:SimpleGame]. ∀[j:Top].  (InitialPos(g@j) ~ j)
BY
{ (Intros THEN UseWitness ⌜Ax⌝⋅ THEN D 1 THEN D 2 THEN D 3 THEN RepUR ``sg-init sg-change-init`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[j:Top].    (InitialPos(g@j)  \msim{}  j)


By

---

Latex:
(Intros
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  D  1
  THEN  D  2
  THEN  D  3
  THEN  RepUR  ``sg-init  sg-change-init``  0
  THEN  Auto)

---

Home Index