proposition: Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x : x ∈ filter P X ↔ P x ∧ x ∈ X.
proof: Proof. unfold filter, set_filter. by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements. Qed.
imports: stdpp(relations) stdpp(options)