---

Step * of Lemma copath-tl_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
  copath-tl(p) ∈ copath(a.B[a];coW-item(w;copath-hd(p))) supposing 0 < copath-length(p)
BY
{ (Auto
   THEN D -2
   THEN RepUR ``copath-length`` -1
   THEN Unfold `coPath` -2
   THEN SplitOnHypITE -2 
   THEN Auto
   THEN D -3
   THEN RepUR ``copath-hd copath-tl`` 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)].
    copath-tl(p)  \mmember{}  copath(a.B[a];coW-item(w;copath-hd(p)))  supposing  0  <  copath-length(p)


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  RepUR  ``copath-length``  -1
  THEN  Unfold  `coPath`  -2
  THEN  SplitOnHypITE  -2 
  THEN  Auto
  THEN  D  -3
  THEN  RepUR  ``copath-hd  copath-tl``  0
  THEN  Auto)

---

Home Index