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` -2
THEN SplitOnHypITE -2
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` -2
THEN SplitOnHypITE -2
THEN Auto)
Home
Index