---

Step * of Lemma update-cubical-context2_wf

No Annotations
∀[ctxt:CubicalContext]. ∀[v:varname()]. ∀[T:Provisional''''(ctt-type-meaning1{i:l}(fst(ctxt)))].
  (ctxt; v:fst(T) ∈ ?CubicalContext)
BY
{ (RepUR ``cubical-context`` 0
   THEN Intros
   THEN Unhide
   THEN Unfold `update-cubical-context2` 0
   THEN (ProvisionCD THENA Auto)
   THEN D 1
   THEN D 2
   THEN Reduce 0
   THEN (GenConclTerm ⌜allow(T)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RepeatFor 2 (D -1)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:CubicalContext].  \mforall{}[v:varname()].  \mforall{}[T:Provisional''''(ctt-type-meaning1\{i:l\}(fst(ctxt)))].
    (ctxt;  v:fst(T)  \mmember{}  ?CubicalContext)


By

---

Latex:
(RepUR  ``cubical-context``  0
  THEN  Intros
  THEN  Unhide
  THEN  Unfold  `update-cubical-context2`  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  RepeatFor  2  (D  -1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index