Nuprl Lemma : bor-to-and

[a,b:𝔹].  {(a ff) ∧ (b ff)} supposing a ∨bff


Proof




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

Latex:
\mforall{}[a,b:\mBbbB{}].    \{(a  \msim{}  ff)  \mwedge{}  (b  \msim{}  ff)\}  supposing  a  \mvee{}\msubb{}b  \msim{}  ff



Date html generated: 2017_10_01-AM-09_12_27
Last ObjectModification: 2017_07_26-PM-04_48_06

Theory : general


Home Index