---

Step * 1 1 of Lemma copathAgree-last


1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ
4. [w] : coW(A;a.B[a])
5. [p] : copath(a.B[a];w)
6. [q] : copath(a.B[a];w)
7. [%] : copath-length(q) ≤ 0
8. [%1] : copathAgree(a.B[a];w;p;q)
9. [%2] : copath-length(q) = (copath-length(p) + 1) ∈ ℤ
⊢ ((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))
BY
{ (Assert ⌜False⌝⋅
   THEN Auto
   THEN (Assert ∃k:ℕ. ((k + 1) ≤ 0) BY
               (D 0 With ⌜copath-length(p)⌝  THEN Auto))
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}
4.  [w]  :  coW(A;a.B[a])
5.  [p]  :  copath(a.B[a];w)
6.  [q]  :  copath(a.B[a];w)
7.  [\%]  :  copath-length(q)  \mleq{}  0
8.  [\%1]  :  copathAgree(a.B[a];w;p;q)
9.  [\%2]  :  copath-length(q)  =  (copath-length(p)  +  1)
\mvdash{}  ((fst(copath-last(w;q)))  =  copath-at(w;p))
\mwedge{}  (copath-at(w;q)  =  coW-item(copath-at(w;p);snd(copath-last(w;q))))


By

---

Latex:
(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (Assert  \mexists{}k:\mBbbN{}.  ((k  +  1)  \mleq{}  0)  BY
                          (D  0  With  \mkleeneopen{}copath-length(p)\mkleeneclose{}    THEN  Auto))
  THEN  D  -1
  THEN  Auto)

---

Home Index