proposition: Lemma munion_perm_left : forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).
proof: Proof. intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym. exact meq_trans. Qed.
imports: PeanoNat Permut Setoid