proposition: Lemma munion_ass : forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
proof: Proof. unfold meq; unfold munion; unfold multiplicity. destruct x; destruct y; destruct z; intros; symmetry; apply Nat.add_assoc. Qed.
imports: PeanoNat Permut Setoid