proposition: Theorem permutation_map_ex : forall (A B : Set) (f : A -> B) l1 l2, permutation (map f l1) l2 -> exists l3, permutation l3 l1 /\ l2 = map f l3.
proof: Proof. intros A0 B f l1 l2 H; apply permutation_map_ex_aux with (l1 := map f l1); auto. Qed.
imports: List ListAux