proposition: Lemma big_cat_uniq xs f y : uniq (\big[cat/[::]]_(x <- xs) f x) -> y \In xs -> uniq (f y).
proof: Proof. elim: xs=>[|x xs IH] in y * => //. rewrite big_cons InE cat_uniq. case/and3P=>U _ Us; case=>[->|Hy] //. by apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)