---

Step * of Lemma cubical-context-lookup_wf

No Annotations
∀[ctxt:?CubicalContext]. ∀[v:varname()].
  (cubical-context-lookup(ctxt;v) ∈ Provisional''''(cttTerm(context-set(ctxt))) supposing context-ok(ctxt))
BY
{ (Intros
   THEN Unhide
   THEN Unfold `uimplies` 0
   THEN (MemTypeCD THENW Auto)
   THEN Unfold `cubical-context-lookup` 0
   THEN (ProvisionCD THENA Auto)) }

1
1. ctxt : ?CubicalContext
2. v : varname()
3. context-ok(ctxt)
4. in-context-dom(allow(ctxt);v) ∈ 𝕌{i''''}
5. ∀[T:𝕌{i'''''}]. ∀[ok:ℙ{i''''}]. ∀[v:⋂:ok. T].  (provision(ok; v) ∈ Provisional''''(T))
6. in-context-dom(allow(ctxt);v)
⊢ cubical_context_val(allow(ctxt);v) ∈ cttTerm(context-set(ctxt))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:?CubicalContext].  \mforall{}[v:varname()].
    (cubical-context-lookup(ctxt;v)  \mmember{}  Provisional''''(cttTerm(context-set(ctxt))) 
                                                                        supposing  context-ok(ctxt))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `uimplies`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Unfold  `cubical-context-lookup`  0
  THEN  (ProvisionCD  THENA  Auto))

---

Home Index