Nuprl Lemma : assert_of_band

p:𝔹. ∀q:⋂:↑p. 𝔹.  uiff(↑(p ∧b q);(↑p) ∧ (↑q))


Proof




Definitions occuring in Statement :  band: p ∧b q assert: b bool: 𝔹 uiff: uiff(P;Q) all: x:A. B[x] and: P ∧ Q isect: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit member: t ∈ T it: btrue: tt uall: [x:A]. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a assert: b ifthenelse: if then else fi  band: p ∧b q bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb false: False prop: subtype_rel: A ⊆B true: True
Lemmas referenced :  eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot true_wf it_wf subtype_rel_self assert_witness assert_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut Error :inhabitedIsType,  hypothesis thin sqequalHypSubstitution unionElimination equalityElimination introduction extract_by_obid isectElimination hypothesisEquality productElimination independent_isectElimination sqequalRule Error :dependent_pairFormation_alt,  Error :equalityIsType1,  promote_hyp dependent_functionElimination instantiate cumulativity equalityTransitivity equalitySymmetry independent_functionElimination because_Cache voidElimination Error :universeIsType,  isectEquality lambdaFormation applyEquality independent_pairFormation Error :isect_memberFormation_alt,  natural_numberEquality independent_pairEquality axiomEquality Error :productIsType,  isect_memberFormation productEquality

Latex:
\mforall{}p:\mBbbB{}.  \mforall{}q:\mcap{}:\muparrow{}p.  \mBbbB{}.    uiff(\muparrow{}(p  \mwedge{}\msubb{}  q);(\muparrow{}p)  \mwedge{}  (\muparrow{}q))



Date html generated: 2019_06_20-AM-11_31_35
Last ObjectModification: 2018_09_28-PM-11_33_03

Theory : bool_1


Home Index