---

Step * of Lemma pcw-path-copathAgree

∀[A:𝕌']. ∀[B:A ⟶ Type].
  ∀w:coW(A;a.B[a]). ∀path:Path.
    (StepAgree(path 0;⋅;w)
    ⇒ (∀i:ℕ
          ((copath-length(pcw-path-coPath(i + 1;path)) = (i + 1) ∈ ℤ)
          ⇒ (copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ)
          ⇒ copathAgree(a.B[a];w;pcw-path-coPath(i;path);pcw-path-coPath(i + 1;path)))))
BY
{ (RepeatFor 6 (Intro)
   THEN (InstLemma `pcw-path-coPath_wf` [⌜A⌝;⌜B⌝;⌜w⌝;⌜path⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜i⌝] (-1)⋅ THENA Auto)
   THEN (D -2 With ⌜i + 1⌝  THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}w:coW(A;a.B[a]).  \mforall{}path:Path.
        (StepAgree(path  0;\mcdot{};w)
        {}\mRightarrow{}  (\mforall{}i:\mBbbN{}
                    ((copath-length(pcw-path-coPath(i  +  1;path))  =  (i  +  1))
                    {}\mRightarrow{}  (copath-length(pcw-path-coPath(i;path))  =  i)
                    {}\mRightarrow{}  copathAgree(a.B[a];w;pcw-path-coPath(i;path);pcw-path-coPath(i  +  1;path)))))


By

---

Latex:
(RepeatFor  6  (Intro)
  THEN  (InstLemma  `pcw-path-coPath\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}path\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}i  +  1\mkleeneclose{}    THENA  Auto))

---

Home Index