proposition: Lemma permutation_map_cons : forall {A} {B} (f: B -> A) {x1 l2} {shuffled: list A}, Permutation shuffled (x1 :: l2) -> forall x1' l2', f x1' = x1 -> List.map f l2' = l2 -> exists l', List.map f l' = shuffled /\ Permutation l' (x1' :: l2').
proof: Proof. intros. replace (x1' :: l2') with ([x1'] ++ l2') by reflexivity. subst; eapply permutation_map_app; eauto; simpl; assumption. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts Coq.Program.Program