Nuprl Lemma : inconsistent-bool-eq3

[b:𝔹]. uiff(b = ¬bb;False)


Proof




Definitions occuring in Statement :  bnot: ¬bb bool: 𝔹 uiff: uiff(P;Q) uall: [x:A]. B[x] false: False equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a bnot: ¬bb ifthenelse: if then else fi  false: False not: ¬A prop: bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} assert: b
Lemmas referenced :  bool_wf eqtt_to_assert btrue_neq_bfalse equal-wf-base false_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bnot_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality thin extract_by_obid hypothesis lambdaFormation sqequalHypSubstitution unionElimination equalityElimination isectElimination productElimination independent_isectElimination sqequalRule independent_pairFormation independent_functionElimination voidElimination baseClosed dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry because_Cache independent_pairEquality isect_memberEquality axiomEquality

Latex:
\mforall{}[b:\mBbbB{}].  uiff(b  =  \mneg{}\msubb{}b;False)



Date html generated: 2017_10_01-AM-09_12_48
Last ObjectModification: 2017_07_26-PM-04_48_23

Theory : general


Home Index