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