Nuprl Lemma : cubical-context_cumulativity
?CubicalContext ⊆r ?CubicalContext'
Proof
Definitions occuring in Statement :
cubical-context: ?CubicalContext,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
cubical-context: ?CubicalContext,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
guard: {T}
Lemmas referenced :
provisional-subtype,
cubical_context_wf,
cubical_context_cumulativity,
provisional-type-cumulativity,
subtype_rel_transitivity,
provisional-type_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesis,
independent_isectElimination
Latex:
?CubicalContext \msubseteq{}r ?CubicalContext'
Date html generated:
2020_05_20-PM-08_04_19
Last ObjectModification:
2020_05_17-PM-10_46_47
Theory : cubical!type!theory
Home
Index