proposition: Lemma IsSetEqSafe_map : forall {A B: Type} (proc: A -> B), IsSetEqSafe (fun x => List.map proc x).
proof: Proof. unfold IsSetEqSafe; eauto using SetEq_after_map. Qed.
imports: Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation Fiat.Common.List.FlattenList Fiat.Common.SetEq