proposition: Lemma perm_domUn f1 f2 : valid (f1 \+ f2) -> perm_eq (dom (f1 \+ f2)) (dom f1 ++ dom f2).
proof: Proof. move=>Vh; apply: uniq_perm; last 1 first. - by move=>x; rewrite mem_cat domUn inE Vh. - by apply: uniq_dom. rewrite cat_uniq !uniq_dom /= andbT; apply/hasPn=>x. rewrite !pcmE /= !umEX /UM.valid /UM.union /UM.dom in Vh *. case: (UMC.from f1) (UMC.from f2) Vh=>// f1' H1 [//|f2' H2]. by case: disjP=>// H _; apply: contraL (H x). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)