Nuprl Lemma : sub-bag-append-left

[T:Type]. ∀b1,b2,b:bag(T).  (sub-bag(T;b1 b2;b)  sub-bag(T;b1;b))


Proof




Definitions occuring in Statement :  sub-bag: sub-bag(T;as;bs) bag-append: as bs bag: bag(T) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q sub-bag: sub-bag(T;as;bs) exists: x:A. B[x] member: t ∈ T top: Top prop:
Lemmas referenced :  bag-append_wf bag-append-assoc equal_wf bag_wf sub-bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut hypothesis dependent_pairFormation introduction extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule isect_memberEquality voidElimination voidEquality because_Cache equalityTransitivity equalitySymmetry hyp_replacement Error :applyLambdaEquality,  universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}b1,b2,b:bag(T).    (sub-bag(T;b1  +  b2;b)  {}\mRightarrow{}  sub-bag(T;b1;b))



Date html generated: 2016_10_25-AM-10_26_31
Last ObjectModification: 2016_07_12-AM-06_42_34

Theory : bags


Home Index