proposition: Lemma undup_filter A f (l : list A) : undup (filter f l) = filter f (undup l).
proof: Proof. induction l; ins; desf; ins; desf; rewrite in_filter_iff in *; clarify_not; desf; congruence. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation