### Nuprl Lemma : bag-drop_wf

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

Proof

Definitions occuring in Statement :  bag-drop: `bag-drop(eq;bs;a)` 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-drop: `bag-drop(eq;bs;a)` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  bag-remove1_wf bag_wf unit_wf2 equal_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis unionEquality lambdaFormation equalityTransitivity equalitySymmetry unionElimination dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality because_Cache universeEquality

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

Date html generated: 2019_10_16-AM-11_31_16
Last ObjectModification: 2018_08_21-PM-01_59_14

Theory : bags_2

Home Index