Nuprl Lemma : bag-member-append

[T:Type]. ∀x:T. ∀as,bs:bag(T).  (x ↓∈ as bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)


Proof




Definitions occuring in Statement :  bag-member: x ↓∈ bs bag-append: as bs bag: bag(T) sq_or: a ↓∨ b uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q universe: Type
Definitions unfolded in proof :  sq_or: a ↓∨ b uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q squash: T exists: x:A. B[x] prop: subtype_rel: A ⊆B uimplies: supposing a bag-append: as bs rev_implies:  Q sq_stable: SqStable(P) or: P ∨ Q bag-member: x ↓∈ bs bag: bag(T) quotient: x,y:A//B[x; y] cand: c∧ B guard: {T}
Lemmas referenced :  bag_to_squash_list bag-member_wf bag-append_wf list-subtype-bag squash_wf or_wf sq_stable__bag-member bag_wf istype-universe member-permutation member_append l_member_wf append_wf permutation_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt introduction cut lambdaFormation_alt independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis equalitySymmetry hyp_replacement applyLambdaEquality rename applyEquality because_Cache independent_isectElimination lambdaEquality_alt inhabitedIsType imageMemberEquality baseClosed universeIsType independent_functionElimination dependent_functionElimination independent_pairEquality functionIsTypeImplies universeEquality pertypeElimination equalityTransitivity unionElimination inlFormation_alt dependent_pairFormation_alt productIsType equalityIsType1 inrFormation_alt

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}as,bs:bag(T).    (x  \mdownarrow{}\mmember{}  as  +  bs  \mLeftarrow{}{}\mRightarrow{}  x  \mdownarrow{}\mmember{}  as  \mdownarrow{}\mvee{}  x  \mdownarrow{}\mmember{}  bs)



Date html generated: 2019_10_15-AM-11_01_13
Last ObjectModification: 2018_10_10-PM-01_06_41

Theory : bags


Home Index