proposition: Lemma findUnL k f1 f2 : valid (f1 \+ f2) -> find k (f1 \+ f2) = if k \in dom f1 then find k f1 else find k f2.
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.find /UM.union /UM.dom. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] //. case: ifP=>// D _; case: ifP=>E1; last first. - rewrite fnd_fcat; case: ifP=>// E2. by rewrite fnd_supp ?E1 // fnd_supp ?E2. suff E2: k \notin supp f2' by rewrite fnd_fcat (negbTE E2). by case: disjP D E1=>// H _; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)