proposition: Lemma flat_map_rev_permutation : forall {A B} seq (f: A -> list B), Permutation (flat_map f seq) (flat_map f (rev seq)).
proof: Proof. induction seq; simpl; intros. - reflexivity. - etransitivity. apply Permutation_app; eauto. clear IHseq; induction (rev seq); simpl; eauto. etransitivity; [ | apply Permutation_app; eauto]. repeat rewrite app_assoc; apply Permutation_app_tail. eauto using Permutation_app_comm. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts Coq.Program.Program Coq.Lists.SetoidList