proposition: Lemma uniq_big_cat xs f : Uniq xs -> (forall x, x \In xs -> uniq (f x)) -> (forall x1 x2, x1 \In xs -> x2 \In xs -> has (mem (f x1)) (f x2) -> x1 = x2) -> uniq (\big[cat/[::]]_(x <- xs) f x).
proof: Proof. elim: xs=>[|x xs IH] /=. - by rewrite big_nil /=; constructor. case=>Nx U H1 H2; rewrite big_cons cat_uniq. apply/and3P; split. - by apply: H1; left. - rewrite has_big_cat -all_predC; apply/allPIn=>x3 H3 /=. by apply: contra_notN Nx=>H; rewrite (H2 _ _ _ _ H) //; [left | right]. apply: IH=>//. - by move=>z Hz; apply: H1; right. by move=>z1 z2 Hz1 Hz2 N; apply: H2=>//; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)