Nuprl Lemma : eqof_equal_btrue

[A:Type]. ∀[d:EqDecider(A)]. ∀[i,j:A].  eqof(d) tt supposing j ∈ A


Proof




Definitions occuring in Statement :  eqof: eqof(d) deq: EqDecider(T) btrue: tt uimplies: supposing a uall: [x:A]. B[x] apply: a universe: Type sqequal: t equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a iff: ⇐⇒ Q and: P ∧ Q implies:  Q true: True prop: rev_implies:  Q uiff: uiff(P;Q) assert: b ifthenelse: if then else fi  btrue: tt sq_type: SQType(T) all: x:A. B[x] guard: {T}
Lemmas referenced :  subtype_base_sq bool_subtype_base iff_imp_equal_bool eqof_wf btrue_wf equal_wf true_wf safe-assert-deq assert_wf iff_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination because_Cache independent_isectElimination hypothesis applyEquality hypothesisEquality independent_pairFormation lambdaFormation natural_numberEquality addLevel productElimination impliesFunctionality dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom sqequalRule isect_memberEquality universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[d:EqDecider(A)].  \mforall{}[i,j:A].    eqof(d)  i  j  \msim{}  tt  supposing  i  =  j



Date html generated: 2016_05_14-AM-06_06_45
Last ObjectModification: 2015_12_26-AM-11_46_42

Theory : equality!deciders


Home Index