proposition: Lemma IsSetEqSafe_filter : forall {A: Type} (pred: A -> bool), IsSetEqSafe (fun x => List.filter pred x).
proof: Proof. unfold IsSetEqSafe, SetEq; intros; repeat rewrite filter_In; specialize (H x); intuition. Qed.
imports: Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation Fiat.Common.List.FlattenList Fiat.Common.SetEq