proposition: Lemma meq_left : forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
proof: Proof. unfold meq; unfold munion; unfold multiplicity. destruct x; destruct y; destruct z. intros; elim H; reflexivity. Qed.
imports: PeanoNat Permut Setoid