Step
*
of Lemma
copath-at_wf
∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. (copath-at(w;p) ∈ coW(A;a.B[a]))
BY
{ ProveWfLemma }
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-at(w;p) \mmember{} coW(A;a.B[a]))
By
Latex:
ProveWfLemma
Home
Index