---

Step * 1 of Lemma cubical-context-lookup_wf


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))
BY
{ Auto }

---

Latex:

---

Latex:

1.  ctxt  :  ?CubicalContext
2.  v  :  varname()
3.  context-ok(ctxt)
4.  in-context-dom(allow(ctxt);v)  \mmember{}  \mBbbU{}\{i''''\}
5.  \mforall{}[T:\mBbbU{}\{i'''''\}].  \mforall{}[ok:\mBbbP{}\{i''''\}].  \mforall{}[v:\mcap{}:ok.  T].    (provision(ok;  v)  \mmember{}  Provisional''''(T))
6.  in-context-dom(allow(ctxt);v)
\mvdash{}  cubical\_context\_val(allow(ctxt);v)  \mmember{}  cttTerm(context-set(ctxt))


By

---

Latex:
Auto

---

Home Index