Nuprl Lemma : bor_ff_simp

[u:𝔹]. u ∨bff u


Proof




Definitions occuring in Statement :  bor: p ∨bq bfalse: ff bool: 𝔹 uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] bor: p ∨bq bool: 𝔹 unit: Unit member: t ∈ T it: btrue: tt ifthenelse: if then else fi  bfalse: ff
Lemmas referenced :  btrue_wf bfalse_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut sqequalRule sqequalHypSubstitution unionElimination thin equalityElimination introduction extract_by_obid hypothesis Error :universeIsType

Latex:
\mforall{}[u:\mBbbB{}].  u  \mvee{}\msubb{}ff  =  u



Date html generated: 2019_06_20-AM-11_31_00
Last ObjectModification: 2018_09_26-AM-11_14_52

Theory : bool_1


Home Index