proposition: Lemma mem_filter a x s : (x \in filter a s) = a x && (x \in s).
proof: Proof. rewrite andbC; elim: s => //= y s IHs. rewrite (fun_if (fun s' : seq T => x \in s')) !in_cons {}IHs. by case: eqP => [->|_]; case (a y); rewrite /= ?andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)