proposition: Lemma big_cat_mem_seq xs f b : b \in \big[cat/[::]]_(x <- xs) f x = has (fun x => b \in f x) xs.
proof: Proof. rewrite -has_pred1 has_big_cat; apply: eq_has=>x. by rewrite has_pred1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)