---

Step * of Lemma sg-legal1-change-init

∀[g:SimpleGame]. ∀[x,y,j:Top].  (Legal1(x;y) ~ Legal1(x;y))
BY
{ (Intros
   THEN UseWitness ⌜Ax⌝⋅
   THEN D 1
   THEN D 2
   THEN D 3
   THEN RepUR ``sg-legal1 sg-normalize sg-change-init`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[x,y,j:Top].    (Legal1(x;y)  \msim{}  Legal1(x;y))


By

---

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

---

Home Index