Nuprl Lemma : cubical-context-lookup_wf
∀[ctxt:?CubicalContext]. ∀[v:varname()].
(cubical-context-lookup(ctxt;v) ∈ Provisional''''(cttTerm(context-set(ctxt))) supposing context-ok(ctxt))
Proof
Definitions occuring in Statement :
cubical-context-lookup: cubical-context-lookup(ctxt;v),
context-set: context-set(ctxt),
context-ok: context-ok(ctxt),
cubical-context: ?CubicalContext,
ctt-term-meaning: cttTerm(X),
varname: varname(),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
provisional-type: Provisional(T)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
cubical-context-lookup: cubical-context-lookup(ctxt;v),
cubical-context: ?CubicalContext,
subtype_rel: A ⊆r B,
prop: ℙ,
context-ok: context-ok(ctxt)
Lemmas referenced :
in-context-dom_wf,
cubical_context_wf,
ctt-term-meaning_wf,
context-set_wf,
context-ok_wf,
varname_wf,
cubical-context_wf,
cubical_context_val_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
isect_memberEquality_alt,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
instantiate,
hypothesis,
because_Cache,
independent_isectElimination,
hypothesisEquality,
applyEquality,
lambdaEquality_alt,
cumulativity,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
sqequalRule,
universeIsType
Latex:
\mforall{}[ctxt:?CubicalContext]. \mforall{}[v:varname()].
(cubical-context-lookup(ctxt;v) \mmember{} Provisional''''(cttTerm(context-set(ctxt)))
supposing context-ok(ctxt))
Date html generated:
2020_05_20-PM-08_11_59
Last ObjectModification:
2020_05_04-PM-03_34_22
Theory : cubical!type!theory
Home
Index