proposition: Lemma map_eqlistA_Proper {A B R} : Proper (pointwise_relation _ R ==> eq ==> SetoidList.eqlistA R) (@List.map A B).
proof: Proof. unfold pointwise_relation. intros f g H ? ls ?; subst. induction ls as [|l ls IHls]; constructor; trivial. Qed.
imports: Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.List.ListFacts Fiat.Common.List.Operations Fiat.Common.List.PermutationFacts Fiat.Common.List.FlattenList