---

Step * of Lemma copath-eta

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
  (0 < copath-length(p) ⇒ (copath-cons(copath-hd(p);copath-tl(p)) = p ∈ copath(a.B[a];w)))
BY
{ Auto }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : copath(a.B[a];w)
5. 0 < copath-length(p)
⊢ copath-cons(copath-hd(p);copath-tl(p)) = p ∈ copath(a.B[a];w)

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p:copath(a.B[a];w)].
    (0  <  copath-length(p)  {}\mRightarrow{}  (copath-cons(copath-hd(p);copath-tl(p))  =  p))


By

---

Latex:
Auto

---

Home Index