---

Step * of Lemma isom-win2

∀g1,g2:SimpleGame.  (g1 ≅ g2 ⇒ {win2(g1) ⇐⇒ win2(g2)})
BY
{ (Auto
   THEN (FLemma `isom-games_inversion` [-1] THENA Auto)
   THEN (D 0 THEN Auto)
   THEN Try ((FLemma `isom-preserves-win2` [-1;-3] THEN Auto))
   THEN FLemma `isom-preserves-win2` [-1;-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g1,g2:SimpleGame.    (g1  \mcong{}  g2  {}\mRightarrow{}  \{win2(g1)  \mLeftarrow{}{}\mRightarrow{}  win2(g2)\})


By

---

Latex:
(Auto
  THEN  (FLemma  `isom-games\_inversion`  [-1]  THENA  Auto)
  THEN  (D  0  THEN  Auto)
  THEN  Try  ((FLemma  `isom-preserves-win2`  [-1;-3]  THEN  Auto))
  THEN  FLemma  `isom-preserves-win2`  [-1;-2]
  THEN  Auto)

---

Home Index