proposition: Lemma big_cat_mem_seqX x (xs : seq A) : reflect (exists2 i, i \in xs & x \in f i) (x \in \big[cat/[::]]_(i <- xs) f i).
proof: Proof. by rewrite big_cat_mem_seq; exact: hasP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)