proposition: Lemma big_cat_uniq_pairwise xs f x1 x2 : uniq (\big[cat/[::]]_(x <- xs) f x) -> x1 \In xs -> x2 \In xs -> has (mem (f x1)) (f x2) -> x1 = x2.
proof: Proof. elim: xs=>[|x xs IH] //. rewrite big_cons cat_uniq; case/and3P=>U N Us. case/In_cons=>[->|H1]; case/In_cons=>[->|H2] //; last by apply: IH. - case/hasP=>/= b Hb1 Hb2. exfalso; move/negP: N; apply. apply/hasP; exists b=>//; rewrite big_cat_mem_seq. by apply/hasPIn; exists x2. case/hasP=>/= b Hb1 Hb2. exfalso; move/negP: N; apply. apply/hasP; exists b=>//; rewrite big_cat_mem_seq. by apply/hasPIn; exists x1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)