---

Step * of Lemma context-ok_wf

No Annotations
∀[ctxt:?CubicalContext]. (context-ok(ctxt) ∈ ℙ{i''''})
BY
{ (Unfolds ``cubical-context context-ok`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:?CubicalContext].  (context-ok(ctxt)  \mmember{}  \mBbbP{}\{i''''\})


By

---

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

---

Home Index