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:  Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q all: x:A. B[x] guard: {T} label: ...$L... t prop: subtype_rel: A ⊆B strong-subtype: strong-subtype(A;B) cand: 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