---

Step * of Lemma copath-eta2

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. ∀[q:coW-dom(a.B[a];w)].
  (0 < copath-length(p)
  ⇒ (q = copath-hd(p) ∈ coW-dom(a.B[a];w))
  ⇒ (copath-cons(q;copath-tl(p)) = p ∈ copath(a.B[a];w)))
BY
{ (InstLemma `copath-eta` [] THEN RepeatFor 4 (ParallelLast') THEN Intros THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `copath-eta`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Intros  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index