---

Step * of Lemma update-cubical-context_wf

No Annotations
∀[ctxt:CubicalContext]. ∀[v:varname()]. ∀[T:Provisional''''(lvl:ℕ4 × {fst(ctxt) ⊢lvl _})].
  (ctxt; v:T ∈ ?CubicalContext)
BY
{ (RepUR ``cubical-context`` 0
   THEN Intros
   THEN Unhide
   THEN Unfold `update-cubical-context` 0
   THEN (ProvisionCD THENA Auto)
   THEN D 1
   THEN D 2
   THEN Reduce 0
   THEN (GenConclTerm ⌜allow(T)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:CubicalContext].  \mforall{}[v:varname()].  \mforall{}[T:Provisional''''(lvl:\mBbbN{}4  \mtimes{}  \{fst(ctxt)  \mvdash{}lvl  \_\})].
    (ctxt;  v:T  \mmember{}  ?CubicalContext)


By

---

Latex:
(RepUR  ``cubical-context``  0
  THEN  Intros
  THEN  Unhide
  THEN  Unfold  `update-cubical-context`  0
  THEN  (ProvisionCD  THENA  Auto)
  THEN  D  1
  THEN  D  2
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}allow(T)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index