proposition: Lemma permut_map : forall f, (Proper (eqA==>eqB) f) -> forall l1 l2, permutation _ eqA_dec l1 l2 -> permutation _ eqB_dec (map f l1) (map f l2).
proof: Proof. intros f; induction l1. - intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl. - intros l2 P. simpl. assert (H0:=permut_cons_InA eqA_equiv P). destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))). subst l2. rewrite map_app. simpl. apply permut_trans with (f b :: map f l1). + revert H1; unfold permutation, meq; simpl. intros; f_equal; auto. destruct (eqB_dec (f b) a0) as [H2|H2]; destruct (eqB_dec (f a) a0) as [H3|H3]; auto. * destruct H3; transitivity (f b); auto with *. * destruct H2; transitivity (f a); auto with *. + apply permut_add_cons_inside. rewrite <- map_app. apply IHl1; auto. apply permut_remove_hd with b; trivial. apply permut_trans with (a::l1); auto. revert H1; unfold permutation, meq; simpl. intros; f_equal; auto. rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto. Qed.
imports: Lia Relations Multiset SetoidList