proposition: Lemma context_list_permut_app2 : forall l l1 l2, list_permut l1 l2 -> list_permut (l1 ++ l) (l2 ++ l).
proof: Proof. intros l l1 l2; unfold list_permut, meq; simpl; intros H a; rewrite (multiplicity_app l1 l); rewrite (multiplicity_app l2 l); rewrite (H a); trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid