proposition: Lemma uniq_rangeUn f1 f2 : valid (f1 \+ f2) -> uniq (range (f1 \+ f2)) = uniq (range f1 ++ range f2).
proof: Proof. move=>W; apply/esym; case: uniq_rangeP=>H; last first. - apply/negP; rewrite cat_uniq=>/and3P [H1 /hasP H2 H3]. elim: H=>k1 k2 v /InUn [] F1 /InUn []; move: F1. - by move/uniq_rangeP: H1; apply. - by move/mem_range=>F1 /mem_range F2; elim: H2; exists v. - by move/mem_range=>F1 /mem_range F2; elim: H2; exists v. by move/uniq_rangeP: H3; apply. rewrite cat_uniq; apply/and3P; split; last 1 first. - by apply/uniq_rangeP=>k1 k2 v F1 F2; apply: (H k1 k2 v); apply/InR. - by apply/uniq_rangeP=>k1 k2 v F1 F2; apply: (H k1 k2 v); apply/InL. case: hasP=>//; case=>x /mem_rangeX [k1 H1] /mem_rangeX [k2 H2]. have [G1 G2] : (k1, x) \In f1 \+ f2 /\ (k2, x) \In f1 \+ f2. - by split; [apply/InR|apply/InL]. rewrite -(H k1 k2 x G1 G2) in H2. by move: (dom_inNR W (In_dom H1)); rewrite (In_dom H2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)