proposition: Lemma SetEq_after_map : forall {A B: Type} (seq1 seq2: list A), forall (proc: A -> B), SetEq seq1 seq2 -> SetEq (map proc seq1) (map proc seq2).
proof: Proof. intros ? ? ? ? ? set_eq; unfold SetEq in *; intro x; split; intros in_map; rewrite in_map_iff in in_map; destruct in_map as [pred (is_pred, pred_in_list)]; specialize (set_eq pred); subst; intuition; eauto using in_map. Qed.
imports: Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation Fiat.Common.List.FlattenList Fiat.Common.SetEq