proposition: Lemma treesort_twist1 : forall x y z t u:multiset, meq u (munion y z) -> meq (munion x (munion u t)) (munion (munion y (munion x t)) z).
proof: Proof. intros; apply meq_trans with (munion x (munion (munion y z) t)). - apply meq_right; apply meq_left; trivial. - apply multiset_twist1. Qed.
imports: PeanoNat Permut Setoid