proposition: Lemma domUn f1 f2 : dom (f1 \+ f2) =i [pred x | valid (f1 \+ f2) & (x \in dom f1) || (x \in dom f2)].
proof: Proof. rewrite !pcmE /= !umEX /UM.dom /UM.valid /UM.union. case: (UMC.from f1) (UMC.from f2)=>[|f1' H1] // [|f2' H2] // x. by case: ifP=>E //; rewrite supp_fcat. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)