proposition: Lemma meq_congr : forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).
proof: Proof. intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right. exact meq_trans. Qed.
imports: PeanoNat Permut Setoid