Nuprl Lemma : bar_wf_base
bar(Base) ∈ Type
Proof
Definitions occuring in Statement :
bar: bar(T),
member: t ∈ T,
base: Base,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a
Lemmas referenced :
bar-wf-base,
base_wf,
subtype_rel_self
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
independent_isectElimination,
because_Cache
Latex:
bar(Base) \mmember{} Type
Date html generated:
2016_05_15-PM-10_03_42
Last ObjectModification:
2015_12_27-PM-05_17_24
Theory : bar!type
Home
Index