proposition: Lemma updUnL k v f1 f2 : upd k v (f1 \+ f2) = if k \in dom f1 then upd k v f1 \+ f2 else f1 \+ upd k v f2.
proof: Proof. rewrite !pcmE /= !umEX /UM.upd /UM.union /UM.dom. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] //=. - by case: ifP=>//; case: decP. case: ifP=>// D; case: ifP=>// H1; case: decP=>// H2. - rewrite disjC disj_ins disjC D !umEX; case: disjP D=>// H _. by rewrite (H _ H1) /= fcat_inss // (H _ H1). - by rewrite disj_ins H1 D /= !umEX fcat_sins. - by rewrite disjC disj_ins disjC D andbF. by rewrite disj_ins D andbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)