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