---

Step * 1 of Lemma coW-is-W


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. coW-wfdd(a.B[a];w)
5. path : Path
6. StepAgree(path 0;⋅;w)
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))
BY
{ ((InstLemma `pcw-path-coPath_wf` [⌜A⌝;⌜B⌝;⌜w⌝;⌜path⌝]⋅ THENA Auto)
   THEN (D 4 With ⌜λn.pcw-path-coPath(n;path)⌝ 
         THENA (Auto
                THEN (InstLemma `pcw-path-copathAgree` [⌜A⌝;⌜B⌝;⌜w⌝;⌜path⌝]⋅ THENA Auto)
                THEN (MemTypeCD THEN Reduce 0)
                THEN Auto
                THEN (InstHyp [⌜i⌝] 6⋅ THEN Auto)
                THEN D 6 With ⌜i + 1⌝ 
                THEN Auto)
         )
   THEN Reduce -1) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ↓∃i:ℕ. (¬(copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ))
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  coW-wfdd(a.B[a];w)
5.  path  :  Path
6.  StepAgree(path  0;\mcdot{};w)
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))


By

---

Latex:
((InstLemma  `pcw-path-coPath\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}path\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  4  With  \mkleeneopen{}\mlambda{}n.pcw-path-coPath(n;path)\mkleeneclose{} 
              THENA  (Auto
                            THEN  (InstLemma  `pcw-path-copathAgree`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}path\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (MemTypeCD  THEN  Reduce  0)
                            THEN  Auto
                            THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  6\mcdot{}  THEN  Auto)
                            THEN  D  6  With  \mkleeneopen{}i  +  1\mkleeneclose{} 
                            THEN  Auto)
              )
  THEN  Reduce  -1)

---

Home Index