Nuprl Lemma : sub-bag-member

[T:Type]. ∀[b1,b2:bag(T)]. ∀[x:T].  (x ↓∈ b2) supposing (sub-bag(T;b1;b2) and x ↓∈ b1)


Definitions occuring in Statement :  bag-member: x ↓∈ bs sub-bag: sub-bag(T;as;bs) bag: bag(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  sub-bag: sub-bag(T;as;bs) exists: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q sq_or: a ↓∨ b or: P ∨ Q prop: squash: T uimplies: supposing a bag-member: x ↓∈ bs
Lemmas referenced :  bag-member-append bag-member_wf sub-bag_wf bag_wf
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin cut hypothesis introduction extract_by_obid isectElimination because_Cache dependent_functionElimination hypothesisEquality independent_functionElimination inlFormation cumulativity sqequalRule imageMemberEquality baseClosed hyp_replacement equalitySymmetry Error :applyLambdaEquality,  universeEquality isect_memberFormation imageElimination isect_memberEquality equalityTransitivity

\mforall{}[T:Type].  \mforall{}[b1,b2:bag(T)].  \mforall{}[x:T].    (x  \mdownarrow{}\mmember{}  b2)  supposing  (sub-bag(T;b1;b2)  and  x  \mdownarrow{}\mmember{}  b1)

Date html generated: 2016_10_25-AM-10_30_23
Last ObjectModification: 2016_07_12-AM-06_46_39

Theory : bags

Home Index