Nuprl Lemma : dl-or?_wf

[x:Prop]. (dl-or?(x) ∈ 𝔹)


Proof




Definitions occuring in Statement :  dl-or?: dl-or?(x) dl-prop: Prop bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dl-or?: dl-or?(x) all: x:A. B[x]
Lemmas referenced :  eq_atom_wf dl-label_wf dl-prop-obj_wf dl-prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality hypothesis tokenEquality axiomEquality equalityTransitivity equalitySymmetry universeIsType

Latex:
\mforall{}[x:Prop].  (dl-or?(x)  \mmember{}  \mBbbB{})



Date html generated: 2019_10_15-AM-11_40_31
Last ObjectModification: 2019_03_26-AM-11_24_41

Theory : dynamic!logic


Home Index