proposition: Lemma permutation_map : forall {A B} f seq seq', Permutation seq' (@map A B f seq) -> exists seq0, seq' = map f seq0.
proof: Proof. induction seq; simpl; intros. exists (@nil A); eauto. symmetry in H; apply Permutation_nil in H; subst; trivial. pose proof (permutation_cons_in H) as f_in. apply in_split in f_in. destruct f_in as [ l1 [ l2 f_in ] ]. subst. rewrite <- Permutation_middle in H. apply Permutation_cons_inv in H. specialize (IHseq _ H). destruct IHseq as [ seq0 IHseq ]. apply app_map_inv in IHseq. destruct IHseq as [ l1' [ l2' (seq0_eq_app & l1l1' & l2l2') ] ]. exists (l1' ++ a :: l2'). rewrite map_app. simpl. subst; intuition. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts