proposition: Lemma list_contents_app : forall l m:list A, meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
proof: Proof. simple induction l; simpl; auto with datatypes. intros. apply meq_trans with (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); auto with datatypes. Qed.
imports: Lia Relations Multiset SetoidList