Nuprl Lemma : bar-base
bar(Base) ⊆r Base
Proof
Definitions occuring in Statement :
bar: bar(T),
subtype_rel: A ⊆r B,
base: Base
Definitions unfolded in proof :
bar: bar(T)
Lemmas referenced :
partial-base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis
Latex:
bar(Base) \msubseteq{}r Base
Date html generated:
2016_05_15-PM-10_03_39
Last ObjectModification:
2016_01_05-PM-06_24_31
Theory : bar!type
Home
Index