proposition: Lemma in_filter_iff A l f (x : A) : In x (filter f l) <-> In x l /\ f x.
proof: Proof. induction l; ins; try tauto. des_if; ins; rewrite IHl; split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation