Step
*
of Lemma
in-context-dom_wf
No Annotations
∀[ctxt:CubicalContext]. ∀[v:varname()].  (in-context-dom(ctxt;v) ∈ ℙ)
BY
{ Auto }
Latex:
Latex:
No  Annotations
\mforall{}[ctxt:CubicalContext].  \mforall{}[v:varname()].    (in-context-dom(ctxt;v)  \mmember{}  \mBbbP{})
By
Latex:
Auto
Home
Index