Nuprl Lemma : assert_of_eq_mset

s:DSet. ∀a,b:MSet{s}.  (↑eq_mset{s}(a,b) ⇐⇒ b ∈ MSet{s})

Proof

Definitions occuring in Statement :  eq_mset: eq_mset{s}(a,b) mset: MSet{s} assert: b all: x:A. B[x] iff: ⇐⇒ Q equal: t ∈ T dset: DSet
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] implies:  Q sq_stable: SqStable(P) mset: MSet{s} iff: ⇐⇒ Q rev_implies:  Q and: P ∧ Q prop: quotient: x,y:A//B[x; y] subtype_rel: A ⊆B so_lambda: λ2y.t[x; y] dset: DSet so_apply: x[s1;s2] uimplies: supposing a squash: T eq_mset: eq_mset{s}(a,b)
Lemmas referenced :  member_wf and_wf assert_of_bpermr quotient-member-eq bpermr_wf equal-wf-base permr_equiv_rel list_wf set_car_wf permr_wf subtype_quotient iff_wf squash_wf sq_stable__equal decidable__assert sq_stable_from_decidable equal_wf eq_mset_wf assert_wf sq_stable__iff dset_wf mset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis isectElimination independent_functionElimination because_Cache introduction pointwiseFunctionalityForEquality sqequalRule pertypeElimination productElimination applyEquality lambdaEquality setElimination rename independent_isectElimination productEquality imageMemberEquality baseClosed independent_pairFormation equalityTransitivity equalitySymmetry imageElimination

Latex:
\mforall{}s:DSet.  \mforall{}a,b:MSet\{s\}.    (\muparrow{}eq\_mset\{s\}(a,b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)

Date html generated: 2016_05_16-AM-07_46_58
Last ObjectModification: 2016_01_16-PM-11_40_19

Theory : mset

Home Index