---

Step * of Lemma update-provisional-context-I_wf

No Annotations
∀[ctxt:?CubicalContext]. ∀[v:varname()].  (ctxt,v:I ∈ ?CubicalContext)
BY
{ (Unfold `cubical-context` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:?CubicalContext].  \mforall{}[v:varname()].    (ctxt,v:I  \mmember{}  ?CubicalContext)


By

---

Latex:
(Unfold  `cubical-context`  0  THEN  ProveWfLemma)

---

Home Index