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