proposition: Lemma list_permut_map : forall f l1 l2, list_permut l1 l2 -> list_permut (map f l1) (map f l2).
proof: Proof. intros f l1; induction l1. intros l2 P; rewrite (list_permut_nil (list_permut_sym P)); apply list_permut_refl. intros l2 P; generalize (split_list_app_cons eq_elt_dec _ _ (cons_permut_in P)); destruct (split_list eq_elt_dec l2 a); intro; subst l2. rewrite map_app; simpl; apply list_permut_add_cons_inside; rewrite <- map_app; apply (IHl1 _ (list_permut_remove_hd l l0 P)). Qed.
imports: decidable_set List more_list Multiset Arith Setoid