Nuprl Lemma : dl-box?_wf

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


Proof




Definitions occuring in Statement :  dl-box?: dl-box?(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-box?: dl-box?(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-box?(x)  \mmember{}  \mBbbB{})



Date html generated: 2019_10_15-AM-11_40_34
Last ObjectModification: 2019_03_26-AM-11_24_42

Theory : dynamic!logic


Home Index