proposition: Lemma permutation_map_app : forall {A} {B} (f: B -> A) {l1 l2} {shuffled: list A}, Permutation shuffled (l1 ++ l2) -> forall l1' l2', List.map f l1' = l1 -> List.map f l2' = l2 -> exists l', List.map f l' = shuffled /\ Permutation l' (l1' ++ l2').
proof: Proof. induction l2; simpl; intros. eapply permutation_map_base; eauto. rewrite map_app; f_equal; assumption. symmetry in H1. apply cons_map_inv in H1. destruct H1 as [ a' [ l2'' ( ? & ? & ? ) ] ]; subst. rewrite <- Permutation_middle in H. pose proof (permutation_cons_in H) as f_in. apply in_split in f_in. destruct f_in as [ s1 [ s2 ? ] ]; subst. rewrite <- Permutation_middle in H. apply Permutation_cons_inv in H. specialize (IHl2 _ H l1' l2'' eq_refl eq_refl). destruct IHl2 as [l' (map_eq & perm)]. symmetry in map_eq. apply app_map_inv in map_eq. destruct map_eq as [ l1'' [ l2''' ( ? & ? & ? ) ] ]; subst. exists (l1'' ++ a' :: l2'''). rewrite map_app; simpl. split; [ trivial | ]. repeat rewrite <- Permutation_middle; eauto. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts