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 ⊆B prop: uimplies: 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