---

Step * 1 2 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. p1 : coPath(a.B[a];w;n)@i
8. b : coW-dom(a.B[a];coPath-at(n;w;p1))@i
⊢ coPathAgree(a.B[a];n;w;p1;coPath-extend(n;p1;b))
BY
{ ((Unfold `coPath` -2 THEN SplitOnHypITE -2  THEN Auto)
   THEN Unfold `coPath-at` -2
   THEN SplitOnHypITE -2 
   THEN Auto
   THEN RepeatFor 2 (Thin (-1))
   THEN D -2
   THEN Reduce -1) }

1
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))

---

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.  p1  :  coPath(a.B[a];w;n)@i
8.  b  :  coW-dom(a.B[a];coPath-at(n;w;p1))@i
\mvdash{}  coPathAgree(a.B[a];n;w;p1;coPath-extend(n;p1;b))


By

---

Latex:
((Unfold  `coPath`  -2  THEN  SplitOnHypITE  -2    THEN  Auto)
  THEN  Unfold  `coPath-at`  -2
  THEN  SplitOnHypITE  -2 
  THEN  Auto
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  D  -2
  THEN  Reduce  -1)

---

Home Index