fact: Fixpoint list_contents (l:list A) : multiset A := match l with | nil => emptyBag | a :: l => munion (singletonBag a) (list_contents l) end.
imports: Coq(List Relations Multiset Arith Setoid) CoLoR(decidable_set more_list equiv_list)