---

Step * of Lemma contextof_wf

No Annotations
∀[X:?CubicalContext]. contextof(X) ∈ CubicalContext supposing context-ok(X)
BY
{ (Unfolds ``cubical-context context-ok contextof`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:?CubicalContext].  contextof(X)  \mmember{}  CubicalContext  supposing  context-ok(X)


By

---

Latex:
(Unfolds  ``cubical-context  context-ok  contextof``  0  THEN  Auto)

---

Home Index