Nuprl Lemma : equal-in-bar
∀[T:Type]. (value-type(T) ⇒ (∀b:bar(T). ∀a:T. ((b = a ∈ bar(T)) ⇒ (b = a ∈ T))))
Proof
Definitions occuring in Statement :
bar: bar(T),
value-type: value-type(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
guard: {T},
label: ...$L... t,
prop: ℙ,
subtype_rel: A ⊆r B,
strong-subtype: strong-subtype(A;B),
cand: A c∧ B
Lemmas referenced :
strong-subtype-bar,
strong-subtype-implies,
equal_wf,
bar_wf,
value-type_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
independent_functionElimination,
hypothesis,
dependent_functionElimination,
hypothesisEquality,
addLevel,
levelHypothesis,
cumulativity,
applyEquality,
productElimination,
sqequalRule,
lambdaEquality,
axiomEquality
Latex:
\mforall{}[T:Type]. (value-type(T) {}\mRightarrow{} (\mforall{}b:bar(T). \mforall{}a:T. ((b = a) {}\mRightarrow{} (b = a))))
Date html generated:
2018_05_21-PM-10_17_29
Last ObjectModification:
2017_07_26-PM-06_36_16
Theory : bar!type
Home
Index