---

Step * of Lemma update-cubical-context-I_wf

No Annotations
∀[ctxt:CubicalContext]. ∀[v:varname()].  (ctxt,v:I ∈ CubicalContext)
BY
{ (Intros THEN Unhide THEN D 1 THEN RepUR ``update-cubical-context-I`` 0 THEN MemCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  1
  THEN  RepUR  ``update-cubical-context-I``  0
  THEN  MemCD
  THEN  Reduce  0
  THEN  Auto)

---

Home Index