Nuprl Lemma : subtype-TYPE
Type ⊆r TYPE
Proof
Definitions occuring in Statement :
subtype_rel: A ⊆r B,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B
Lemmas referenced :
istype-universe
Rules used in proof :
hypothesis,
universeEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
instantiate,
cut,
lambdaEquality_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
universeMemberTYPE,
cumulativity,
hypothesisEquality
Latex:
Type \msubseteq{}r TYPE
Date html generated:
2019_10_15-AM-10_20_39
Last ObjectModification:
2019_08_20-PM-05_10_38
Theory : subtype_1
Home
Index