---

Step * of Lemma coW-equiv-implies

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
    (coW-equiv(a.B[a];w;w') ⇒ (∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇒ coWmem(a.B[a];z;w'))))
BY
{ ((Auto THEN All (Unfolds ``coW-equiv coWmem``))
   THEN D -1
   THEN (RWO "win2-iff" (-4) THENA Auto)
   THEN (D -4 With ⌜<copath-cons(b;()), ()>⌝  THENA ((MemTypeCD THENW Auto) THEN RepUR ``sg-pos sg-legal1 coW-game`` 0 T\000CHEN Auto))
   THEN D -1
   THEN D -2
   THEN RepUR ``sg-pos coW-game`` -3
   THEN D -3
   THEN RepUR ``sg-legal2 coW-game`` -2
   THEN (Assert (copath-cons(b;()) = q1 ∈ copath(a.B[a];w)) ∧ (copath-length(q2) = 1 ∈ ℤ) BY
               ((Subst' copath-length(copath-cons(b;())) + 1 ~ 2 -2 THENA Computation)
                THEN (Unhide THENA Auto)
                THEN ExRepD
                THEN SplitOrHyps
                THEN Auto
                THEN (Eliminate ⌜q2⌝⋅ THENA Auto)
                THEN (Assert copath-length(()) = 2 ∈ ℤ BY
                            Eq)
                THEN RepUR ``copath-length copath-nil`` -1
                THEN Auto))
   THEN Thin (-3)
   THEN D -1) }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. z : coW(A;a.B[a])
6. b : coW-dom(a.B[a];w)
7. coW-equiv(a.B[a];z;coW-item(w;b))
8. q1 : copath(a.B[a];w)
9. q2 : copath(a.B[a];w')
10. win2(coW-game(a.B[a];w;w')@<q1, q2>)
11. copath-cons(b;()) = q1 ∈ copath(a.B[a];w)
12. copath-length(q2) = 1 ∈ ℤ
⊢ ∃b:coW-dom(a.B[a];w'). coW-equiv(a.B[a];z;coW-item(w';b))

---

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{}  (\mforall{}z:coW(A;a.B[a]).  (coWmem(a.B[a];z;w)  {}\mRightarrow{}  coWmem(a.B[a];z;w'))))


By

---

Latex:
((Auto  THEN  All  (Unfolds  ``coW-equiv  coWmem``))
  THEN  D  -1
  THEN  (RWO  "win2-iff"  (-4)  THENA  Auto)
  THEN  (D  -4  With  \mkleeneopen{}<copath-cons(b;()),  ()>\mkleeneclose{} 
              THENA  ((MemTypeCD  THENW  Auto)  THEN  RepUR  ``sg-pos  sg-legal1  coW-game``  0  THEN  Auto)
              )
  THEN  D  -1
  THEN  D  -2
  THEN  RepUR  ``sg-pos  coW-game``  -3
  THEN  D  -3
  THEN  RepUR  ``sg-legal2  coW-game``  -2
  THEN  (Assert  (copath-cons(b;())  =  q1)  \mwedge{}  (copath-length(q2)  =  1)  BY
                          ((Subst'  copath-length(copath-cons(b;()))  +  1  \msim{}  2  -2  THENA  Computation)
                            THEN  (Unhide  THENA  Auto)
                            THEN  ExRepD
                            THEN  SplitOrHyps
                            THEN  Auto
                            THEN  (Eliminate  \mkleeneopen{}q2\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (Assert  copath-length(())  =  2  BY
                                                    Eq)
                            THEN  RepUR  ``copath-length  copath-nil``  -1
                            THEN  Auto))
  THEN  Thin  (-3)
  THEN  D  -1)

---

Home Index