### 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