proposition: Lemma multiset_twist2 : forall x y z t:multiset, meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).
proof: Proof. intros; apply meq_trans with (munion (munion x (munion y z)) t). - apply meq_sym; apply munion_ass. - apply meq_left; apply munion_perm_left. Qed.
imports: PeanoNat Permut Setoid