Nuprl Lemma : sqeqff_to_assert

[b:𝔹]. uiff(b ff;↑¬bb)


Proof




Definitions occuring in Statement :  bnot: ¬bb assert: b bfalse: ff bool: 𝔹 uiff: uiff(P;Q) uall: [x:A]. B[x] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a assert: b ifthenelse: if then else fi  bnot: ¬bb bfalse: ff btrue: tt true: True all: x:A. B[x] implies:  Q bool: 𝔹 prop: false: False subtype_rel: A ⊆B unit: Unit it: sq_type: SQType(T) guard: {T}
Lemmas referenced :  true_wf false_wf equal_wf bool_subtype_base subtype_base_sq bool_wf bfalse_wf assert_wf bnot_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis natural_numberEquality sqequalRule sqequalHypSubstitution thin because_Cache lambdaFormation unionElimination axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination hypothesisEquality dependent_functionElimination independent_functionElimination sqequalIntensionalEquality applyEquality baseClosed instantiate cumulativity independent_isectElimination equalityElimination voidElimination sqequalAxiom productElimination independent_pairEquality isect_memberEquality

Latex:
\mforall{}[b:\mBbbB{}].  uiff(b  \msim{}  ff;\muparrow{}\mneg{}\msubb{}b)



Date html generated: 2017_04_14-AM-07_14_14
Last ObjectModification: 2017_02_27-PM-02_49_59

Theory : union


Home Index