---

Step * 1 of Lemma copathAgree-cons


1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. [b] : coW-dom(a.B[a];w)
5. n : ℕ
6. p1 : coPath(a.B[a];coW-item(w;b);n)
7. n1 : ℕ
8. q1 : coPath(a.B[a];coW-item(w;b);n1)
9. coPathAgree(a.B[a];n;coW-item(w;b);p1;q1)
10. n < n1
11. n + 1 < n1 + 1
⊢ coPathAgree(a.B[a];n + 1;w;<b, p1>;<b, q1>)
BY
{ (Unfold `coPathAgree` 0 THEN Reduce 0 THEN AutoSplit THEN Auto THEN Subst' (n + 1) - 1 ~ n 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [w]  :  coW(A;a.B[a])
4.  [b]  :  coW-dom(a.B[a];w)
5.  n  :  \mBbbN{}
6.  p1  :  coPath(a.B[a];coW-item(w;b);n)
7.  n1  :  \mBbbN{}
8.  q1  :  coPath(a.B[a];coW-item(w;b);n1)
9.  coPathAgree(a.B[a];n;coW-item(w;b);p1;q1)
10.  n  <  n1
11.  n  +  1  <  n1  +  1
\mvdash{}  coPathAgree(a.B[a];n  +  1;w;<b,  p1><b,  q1>)


By

---

Latex:
(Unfold  `coPathAgree`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto
  THEN  Subst'  (n  +  1)  -  1  \msim{}  n  0
  THEN  Auto)

---

Home Index