proposition: Lemma permut_In_In : forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
proof: Proof. unfold PermutSetoid.permutation, meq; intros l1 l2 e P IN. generalize (P e); clear P. destruct (In_dec eq_dec e l2) as [H|H]; auto. rewrite (multiplicity_In_O _ _ H). intros. generalize (multiplicity_In_S _ _ IN). rewrite H0. inversion 1. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation