Nuprl Lemma : eq_bool_tt

[b:𝔹]. =b tt b


Proof




Definitions occuring in Statement :  eq_bool: =b q btrue: tt bool: 𝔹 uall: [x:A]. B[x] 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 sq_type: SQType(T) all: x:A. B[x] guard: {T} assert: b ifthenelse: if then else fi  btrue: tt true: True prop: rev_implies:  Q uiff: uiff(P;Q)
Lemmas referenced :  iff_imp_equal_bool eq_bool_wf btrue_wf subtype_base_sq bool_wf bool_subtype_base equal_wf assert_wf true_wf assert_of_eq_bool iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination independent_pairFormation lambdaFormation instantiate cumulativity dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination natural_numberEquality sqequalRule addLevel productElimination impliesFunctionality because_Cache

Latex:
\mforall{}[b:\mBbbB{}].  b  =b  tt  =  b



Date html generated: 2016_05_15-PM-03_26_12
Last ObjectModification: 2015_12_27-PM-01_07_21

Theory : general


Home Index