Nuprl Lemma : ctt-context-term-mng_wf
∀[X:?CubicalContext]. ∀[t:CttTerm]. (ctt-context-term-mng{i:l}(X;t) ∈ [[X;t]])
Proof
Definitions occuring in Statement :
ctt-context-term-mng: ctt-context-term-mng{i:l}(X;t),
ctt_meaning: [[ctxt;t]],
ctt-term: CttTerm,
cubical-context: ?CubicalContext,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ctt-context-term-mng: ctt-context-term-mng{i:l}(X;t),
so_lambda: so_lambda4,
all: ∀x:A. B[x],
and: P ∧ Q,
so_lambda: λ2x y.t[x; y],
pi2: snd(t),
so_apply: x[s1;s2],
ctt-meaning-triple: CttMeaningTriple,
prop: ℙ,
pi1: fst(t),
ctt-term: CttTerm,
wfterm: wfterm(opr;sort;arity),
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
so_apply: x[s1;s2;s3;s4],
so_lambda: so_lambda3,
varterm: varterm(v),
ctt_meaning: [[ctxt;t]],
ctt-meaning-type: ctt-meaning-type{i:l}(X;t),
isvarterm: isvarterm(t),
isl: isl(x),
ifthenelse: if b then t else f fi ,
btrue: tt,
so_apply: x[s1;s2;s3]
Lemmas referenced :
wfterm-accum_wf_ctt1,
vdf-eq_wf,
cubical-context_wf,
list_wf,
varname_wf,
ctt-term_wf,
ctt_meaning_wf,
ctt-binder-context_wf,
assert_wf,
wf-term_wf,
ctt-op_wf,
ctt-kind_wf,
term_wf,
ctt-arity_wf,
mkterm_wf,
map_wf,
ctt-meaning-triple_wf,
ctt-op-meaning_wf,
pi2_wf,
istype-assert,
cubical-context-lookup_wf,
not_wf,
equal-wf-T-base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality_alt,
lambdaFormation_alt,
productEquality,
instantiate,
hypothesis,
closedConclusion,
cumulativity,
hypothesisEquality,
productElimination,
productIsType,
inhabitedIsType,
dependent_functionElimination,
applyEquality,
universeIsType,
because_Cache,
independent_pairEquality,
setElimination,
rename,
equalityTransitivity,
equalitySymmetry,
dependent_set_memberEquality_alt,
setIsType,
functionExtensionality,
setEquality,
baseClosed
Latex:
\mforall{}[X:?CubicalContext]. \mforall{}[t:CttTerm]. (ctt-context-term-mng\{i:l\}(X;t) \mmember{} [[X;t]])
Date html generated:
2020_05_21-AM-10_47_10
Last ObjectModification:
2020_05_18-AM-11_42_57
Theory : cubical!type!theory
Home
Index