Nuprl Lemma : bool-deq-aux

[a,b:𝔹].  uiff(a b;↑=b b)


Proof




Definitions occuring in Statement :  eq_bool: =b q assert: b bool: 𝔹 uiff: uiff(P;Q) uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T prop: uall: [x:A]. B[x] rev_implies:  Q implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  equal_wf bool_wf iff_weakening_uiff assert_wf eq_bool_wf assert_of_eq_bool assert_witness uiff_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache addLevel productElimination independent_isectElimination independent_functionElimination cumulativity sqequalRule independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry axiomEquality

Latex:
\mforall{}[a,b:\mBbbB{}].    uiff(a  =  b;\muparrow{}a  =b  b)



Date html generated: 2019_06_20-PM-00_31_59
Last ObjectModification: 2018_08_24-PM-10_58_41

Theory : equality!deciders


Home Index