proposition: Lemma mem_filter_eq : forall x P l, mem x (filter P l) = (mem x l /\ P x).
proof: Proof. Proof using. intros. extens. induction l. { rewrite filter_nil. iff M (M&?); inverts M. } { rewrite filter_cons. case_if; rew_listx; rewrite IHl. { iff [M|M] N; subst*. } { iff M ([N|N]&K); subst*. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)