---

Step * 2 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. ¬n + 1 < n1 + 1
9. q1 : coPath(a.B[a];coW-item(w;b);n1)
10. coPathAgree(a.B[a];n1;coW-item(w;b);p1;q1)
11. ¬n < n1
⊢ coPathAgree(a.B[a];n1 + 1;w;<b, p1>;<b, q1>)
BY
{ (Unfold `coPathAgree` 0 THEN Reduce 0 THEN AutoSplit THEN Auto THEN Subst' (n1 + 1) - 1 ~ n1 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.  \mneg{}n  +  1  <  n1  +  1
9.  q1  :  coPath(a.B[a];coW-item(w;b);n1)
10.  coPathAgree(a.B[a];n1;coW-item(w;b);p1;q1)
11.  \mneg{}n  <  n1
\mvdash{}  coPathAgree(a.B[a];n1  +  1;w;<b,  p1><b,  q1>)


By

---

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

---

Home Index