Nuprl Lemma : dl-and-2_wf

[x:Prop]. dl-and-2(x) ∈ Prop supposing ↑dl-and?(x)


Proof




Definitions occuring in Statement :  dl-and-2: dl-and-2(x) dl-and?: dl-and?(x) dl-prop: Prop assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T dl-prop: Prop mrec: mrec(L;i) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] eager-map: eager-map(f;as) list_ind: list_ind outl: outl(x) apply-alist: apply-alist(eq;L;x) dl-Spec: dl-Spec() cons: [a b] ifthenelse: if then else fi  atom-deq: AtomDeq eq_atom: =a y pi1: fst(t) bfalse: ff btrue: tt pi2: snd(t) nil: [] it: iff: ⇐⇒ Q implies:  Q or: P ∨ Q sq_type: SQType(T) guard: {T} mrec-spec: mrec-spec(L;lbl;p) top: Top mk-prec: mk-prec(lbl;x) dl-aprop: atm(x) assert: b dl-and?: dl-and?(x) dl-label: dl-label(d) mobj-label: mobj-label(x) prec-label: prec-label(x) mobj-data: mobj-data(x) dl-prop-obj: prop(x) false: False unit: Unit dl-false: 0 dl-implies: x1  x dl-and: x1 ∧ x true: True dl-and-2: dl-and-2(x) select-tuple: x.n eq_int: (i =z j) subtract: m dl-or: x1 ∨ x dl-prog: Prog dl-box: [x1] x dl-diamond: <x1> x
Lemmas referenced :  prec-ext mrec-spec_wf dl-Spec_wf istype-atom mrec-label-cases1-ext cons_member cons_wf nil_wf subtype_base_sq atom_subtype_base atomdeq_reduce_lemma istype-void map_cons_lemma map_nil_lemma tupletype_cons_lemma null_nil_lemma tupletype_nil_lemma null_cons_lemma member_singleton istype-assert dl-and?_wf dl-prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalHypSubstitution introduction extract_by_obid isectElimination thin atomEquality sqequalRule lambdaEquality_alt hypothesis hypothesisEquality inhabitedIsType tokenEquality promote_hyp hypothesis_subsumption productElimination applyEquality dependent_functionElimination setElimination rename independent_functionElimination unionElimination instantiate cumulativity independent_isectElimination equalityTransitivity equalitySymmetry isect_memberEquality_alt voidElimination equalityElimination universeIsType

Latex:
\mforall{}[x:Prop].  dl-and-2(x)  \mmember{}  Prop  supposing  \muparrow{}dl-and?(x)



Date html generated: 2019_10_15-AM-11_41_25
Last ObjectModification: 2019_03_26-AM-11_24_58

Theory : dynamic!logic


Home Index