proposition: Lemma nodup_filterP A (l: list A) (ND: NoDup l) f : NoDup (filterP f l).
proof: Proof. induction l; ins; inv ND; desf; eauto using NoDup. econstructor; eauto; rewrite in_filterP_iff; tauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation