---

Step * 1 2 1 of Lemma copathAgree-extend


1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ@i
4. [%1] : 0 < n@i
5. ∀w:coW(A;a.B[a]). ∀p1:coPath(a.B[a];w;n - 1). ∀b:coW-dom(a.B[a];coPath-at(n - 1;w;p1)).
     coPathAgree(a.B[a];n - 1;w;p1;coPath-extend(n - 1;p1;b))
6. w : coW(A;a.B[a])@i'
7. t : coW-dom(a.B[a];w)@i
8. p2 : coPath(a.B[a];coW-item(w;t);n - 1)@i
9. b : coW-dom(a.B[a];coPath-at(n - 1;coW-item(w;t);p2))@i
⊢ coPathAgree(a.B[a];n;w;<t, p2>;coPath-extend(n;<t, p2>;b))
BY
{ ((Unfold `coPath-extend` 0 THEN AutoSplit) THEN Unfold `coPathAgree` 0 THEN AutoSplit THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}@i
4.  [\%1]  :  0  <  n@i
5.  \mforall{}w:coW(A;a.B[a]).  \mforall{}p1:coPath(a.B[a];w;n  -  1).  \mforall{}b:coW-dom(a.B[a];coPath-at(n  -  1;w;p1)).
          coPathAgree(a.B[a];n  -  1;w;p1;coPath-extend(n  -  1;p1;b))
6.  w  :  coW(A;a.B[a])@i'
7.  t  :  coW-dom(a.B[a];w)@i
8.  p2  :  coPath(a.B[a];coW-item(w;t);n  -  1)@i
9.  b  :  coW-dom(a.B[a];coPath-at(n  -  1;coW-item(w;t);p2))@i
\mvdash{}  coPathAgree(a.B[a];n;w;<t,  p2>coPath-extend(n;<t,  p2>b))


By

---

Latex:
((Unfold  `coPath-extend`  0  THEN  AutoSplit)  THEN  Unfold  `coPathAgree`  0  THEN  AutoSplit  THEN  Auto)

---

Home Index