proposition: Lemma domU k v f : dom (upd k v f) =i [pred x | C k & if x == k then valid f else x \in dom f].
proof: Proof. rewrite pcmE /= !umEX /UM.dom /UM.upd /UM.valid /=. case: (UMC.from f)=>[|f' H] /= x. - by rewrite !inE /= andbC; case: ifP. case: decP; first by move=>->; rewrite supp_ins. by move/(introF idP)=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)