---

Step * of Lemma coW-equiv_weakening

∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).  coW-equiv(a.B[a];w;w') supposing w = w' ∈ coW(A;a.B[a])
BY
{ (Auto
   THEN ((RWO "-1" 0 THENA Auto) THEN Unfold `coW-equiv` 0)
   THEN BLemma `implies-sg-win2`
   THEN Auto
   THEN RepUR ``coW-game sg-pos sg-legal1 sg-legal2`` 0
   THEN D 0 With ⌜λp.let u,v = p 
                     in u = v ∈ copath(a.B a;w')⌝ 
   THEN Auto
   THEN RepUR ``so_apply`` 0) }

1
1. [A] : 𝕌'
2. B : A ⟶ Type@i'
3. w : coW(A;a.B[a])@i'
4. w' : coW(A;a.B[a])@i'
5. w = w' ∈ coW(A;a.B[a])
⊢ ∃F:p:{p:copath(a.B a;w') × copath(a.B a;w')| let u,v = p in u = v ∈ copath(a.B a;w')} 
     ⟶ q:{q:copath(a.B a;w') × copath(a.B a;w')| 
           let u,v = p 
           in let u',v' = q 
              in ((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                 ∧ copathAgree(a.B a;w';u;u')
                 ∧ (v = v' ∈ copath(a.B a;w')))
                 ∨ ((u = u' ∈ copath(a.B a;w'))
                   ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                   ∧ copathAgree(a.B a;w';v;v'))} 
     ⟶ (copath(a.B a;w') × copath(a.B a;w'))
   ((() = () ∈ copath(a.B a;w'))
   ∧ (∀p:{p:copath(a.B a;w') × copath(a.B a;w')| let u,v = p in u = v ∈ copath(a.B a;w')} .
      ∀q:{q:copath(a.B a;w') × copath(a.B a;w')| 
          let u,v = p 
          in let u',v' = q 
             in ((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                ∧ copathAgree(a.B a;w';u;u')
                ∧ (v = v' ∈ copath(a.B a;w')))
                ∨ ((u = u' ∈ copath(a.B a;w'))
                  ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                  ∧ copathAgree(a.B a;w';v;v'))} .
        (let u,v = F p q 
         in u = v ∈ copath(a.B a;w')
        ∧ let u,v = q 
          in let u',v' = F p q 
             in (((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                ∧ copathAgree(a.B a;w';u;u')
                ∧ (v = v' ∈ copath(a.B a;w')))
                ∨ ((u = u' ∈ copath(a.B a;w'))
                  ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                  ∧ copathAgree(a.B a;w';v;v')))
                ∧ (copath-length(u') = copath-length(v') ∈ ℤ))))

---

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')  supposing  w  =  w'


By

---

Latex:
(Auto
  THEN  ((RWO  "-1"  0  THENA  Auto)  THEN  Unfold  `coW-equiv`  0)
  THEN  BLemma  `implies-sg-win2`
  THEN  Auto
  THEN  RepUR  ``coW-game  sg-pos  sg-legal1  sg-legal2``  0
  THEN  D  0  With  \mkleeneopen{}\mlambda{}p.let  u,v  =  p 
                                      in  u  =  v\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0)

---

Home Index