Nuprl Lemma : top-subtype-record
Top ⊆r record(x.Top)
Proof
Definitions occuring in Statement :
record: record(x.T[x]),
subtype_rel: A ⊆r B,
top: Top
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T,
record: record(x.T[x]),
top: Top
Lemmas referenced :
istype-void,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality_alt,
functionExtensionality,
isect_memberEquality_alt,
voidElimination,
cut,
introduction,
extract_by_obid,
hypothesis,
closedConclusion,
atomEquality
Latex:
Top \msubseteq{}r record(x.Top)
Date html generated:
2019_10_15-AM-11_28_10
Last ObjectModification:
2018_10_22-PM-03_37_58
Theory : general
Home
Index