---

Step * of Lemma coPath-at_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[p:coPath(a.B[a];w;n)].  (coPath-at(n;w;p) ∈ coW(A;a.B[a]))
BY
{ (InductionOnNat
   THEN Auto
   THEN Unfold `coPath-at` 0
   THEN Reduce 0
   THEN Auto
   THEN Unfold `coPath` -1
   THEN SplitOnHypITE -1 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p:coPath(a.B[a];w;n)].
    (coPath-at(n;w;p)  \mmember{}  coW(A;a.B[a]))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  Unfold  `coPath-at`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Unfold  `coPath`  -1
  THEN  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index