fact: Fixpoint list2multiset (l : list A) : Multiset := match l with | List.nil => empty | List.cons x xs => insert x (list2multiset xs) end.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)