---

Step * of Lemma coPath-extend_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[p:coPath(a.B[a];w;n)]. ∀[t:coW-dom(a.B[a];coPath-at(n;w;p))].
  (coPath-extend(n;p;t) ∈ coPath(a.B[a];w;n + 1))
BY
{ ((InductionOnNat THEN Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN Unfold `coPath-extend` 0
   THEN Unfold `coPath` 0
   THEN Unfold `coPath-at` 0
   THEN Reduce 0
   THEN Try (SplitOnConclITE)
   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)].
\mforall{}[t:coW-dom(a.B[a];coPath-at(n;w;p))].
    (coPath-extend(n;p;t)  \mmember{}  coPath(a.B[a];w;n  +  1))


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  Unfold  `coPath-extend`  0
  THEN  Unfold  `coPath`  0
  THEN  Unfold  `coPath-at`  0
  THEN  Reduce  0
  THEN  Try  (SplitOnConclITE)
  THEN  Auto)

---

Home Index