Nuprl Lemma : ctt-meaning-triple_wf
CttMeaningTriple ∈ 𝕌{i'''''}
Proof
Definitions occuring in Statement :
ctt-meaning-triple: CttMeaningTriple,
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
ctt-meaning-triple: CttMeaningTriple,
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
cubical-context_wf,
list_wf,
varname_wf,
ctt-term_wf,
ctt_meaning_wf,
pi2_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
productEquality,
cut,
introduction,
extract_by_obid,
hypothesis,
cumulativity,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
instantiate,
lambdaEquality_alt,
universeIsType
Latex:
CttMeaningTriple \mmember{} \mBbbU{}\{i'''''\}
Date html generated:
2020_05_21-AM-10_34_19
Last ObjectModification:
2020_03_18-PM-02_48_52
Theory : cubical!type!theory
Home
Index