### Nuprl Lemma : bag-remove_wf

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  (bs - x ∈ bag(T))`

Proof

Definitions occuring in Statement :  bag-remove: `bs - x` bag: `bag(T)` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag-remove: `bs - x` so_lambda: `λ2x.t[x]` deq: `EqDecider(T)` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` uimplies: `b supposing a`
Lemmas referenced :  bag-filter_wf bnot_wf subtype_rel_bag assert_wf bag_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality applyEquality setElimination rename hypothesis because_Cache setEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    (bs  -  x  \mmember{}  bag(T))

Date html generated: 2016_05_15-PM-08_03_15
Last ObjectModification: 2015_12_27-PM-04_15_20

Theory : bags_2

Home Index