proposition: Lemma updR k v f1 f2 : k \in dom f2 -> upd k v (f1 \+ f2) = f1 \+ upd k v f2.
proof: Proof. by move=>D; rewrite updUnR D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)