proposition: Lemma Permutation_map_ex_aux : forall (A B : Set) (f : A -> B) l1 l2 l3, Permutation l1 l2 -> l1 = map f l3 -> exists l4, Permutation l4 l3 /\ l2 = map f l4.
proof: Proof. intros A B f l1 l2 l3 H H0. assert (exists l4 : list A, l2 = map f l4 /\ Permutation l4 l3). { rewrite H0 in H. apply Permutation_sym in H. epose proof (Permutation_map_inv f _ H). destruct H1; auto. now exists x. } destruct H1. now exists x. Qed.
imports: List ListAux