---

Step * of Lemma coW-equiv_inversion

∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ coW-equiv(a.B[a];w';w))
BY
{ (Auto
   THEN ParallelLast
   THEN InstLemma `isom-preserves-win2` [⌜coW-game(a.B[a];w;w')⌝;⌜coW-game(a.B[a];w';w)⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. win2(coW-game(a.B[a];w;w'))
⊢ coW-game(a.B[a];w;w') ≅ coW-game(a.B[a];w';w)

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w,w':coW(A;a.B[a]).    (coW-equiv(a.B[a];w;w')  {}\mRightarrow{}  coW-equiv(a.B[a];w';w))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  InstLemma  `isom-preserves-win2`  [\mkleeneopen{}coW-game(a.B[a];w;w')\mkleeneclose{};\mkleeneopen{}coW-game(a.B[a];w';w)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index