proposition: Lemma uniq_big_catP (xs : seq A) : reflect [/\ forall i, i \in xs -> uniq (f i), forall i k, i \in xs -> k \in f i -> count_mem i xs = 1 & forall i j k, i \in xs -> j \in xs -> k \in f i -> k \in f j -> i = j] (uniq (\big[cat/[::]]_(i <- xs) f i)).
proof: Proof. elim: xs=>[|x xs IH] /=; first by rewrite big_nil; constructor. rewrite big_cons cat_uniq. case H1 : (uniq (f x))=>/=; last first. - by constructor; case=>/(_ x); rewrite inE eqxx H1=>/(_ erefl). case: hasPn=>/= V; last first. - constructor; case=>H2 H3 H4; elim: V=>z /big_cat_mem_seqX [i X Zi]. apply/negP=>Zx; move/(H3 i z): (Zi); rewrite inE X orbT=>/(_ erefl). move: (H4 x i z); rewrite !inE eqxx X orbT=>/(_ erefl erefl Zx Zi)=>E. by rewrite -{i Zi}E eqxx add1n in X *; case=>/count_memPn; rewrite X. case: IH=>H; constructor; last first. - case=>H2 H3 H4; apply: H; split; last 1 first. - by move=>i j k Xi Xj; apply: H4; rewrite inE ?Xi ?Xj orbT. - by move=>i X; apply: H2; rewrite inE X orbT. move=>i k X D; move/(H3 i k): (D); rewrite inE X orbT=>/(_ erefl). case: (x =P i) X D=>[<-{i}|N] X D; last by rewrite add0n. by rewrite add1n=>[[]] /count_memPn; rewrite X. case: H=>H2 H3 H4; split; first by move=>i; rewrite inE=>/orP [/eqP ->|/H2]. - move=>i k; rewrite inE eq_sym; case: (x =P i)=>[<- _|N /= Xi] K; last first. - by rewrite add0n; apply: H3 Xi K. rewrite add1n; congr S; apply/count_memPn; apply: contraL (K)=>X. by apply/V/big_cat_mem_seqX; exists x. move=>i j k; rewrite !inE=>/orP [/eqP ->{i}|Xi] /orP [/eqP ->{j}|Xj] Ki Kj //. - by suff : k \notin f x; [rewrite Ki | apply/V/big_cat_mem_seqX; exists j]. - by suff : k \notin f x; [rewrite Kj | apply/V/big_cat_mem_seqX; exists i]. by apply: H4 Kj. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)