proposition: Lemma list_permut_app_app : forall l1 l2, list_permut (l1 ++ l2) (l2 ++ l1).
proof: Proof. intros l1 l2; unfold list_permut, meq; intro a; rewrite multiplicity_app; rewrite multiplicity_app; apply plus_comm. Qed.
imports: decidable_set List more_list Multiset Arith Setoid