Nuprl Lemma : inconsistent-bool-eq

uiff(tt ff;False)


Proof




Definitions occuring in Statement :  bfalse: ff btrue: tt bool: 𝔹 uiff: uiff(P;Q) false: False equal: t ∈ T
Definitions unfolded in proof :  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T false: False not: ¬A implies:  Q prop: uall: [x:A]. B[x]
Lemmas referenced :  btrue_neq_bfalse equal_wf bool_wf btrue_wf bfalse_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut hypothesis thin lemma_by_obid sqequalHypSubstitution independent_functionElimination voidElimination sqequalRule isectElimination

Latex:
uiff(tt  =  ff;False)



Date html generated: 2016_05_15-PM-03_27_28
Last ObjectModification: 2015_12_27-PM-01_08_26

Theory : general


Home Index