proposition: Lemma permutation_map : forall f l1 l2, permutation l1 l2 -> PermutSetoid.permutation _ eqB_dec (map f l1) (map f l2).
proof: Proof. intros f; induction l1. - intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl. - intros l2 P. simpl. destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)). subst l2. rewrite map_app. simpl. apply permut_add_cons_inside. rewrite <- map_app. apply IHl1; auto. apply permut_remove_hd with a; auto with typeclass_instances. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation