proposition: Lemma size_domU k v f : valid (upd k v f) -> size (dom (upd k v f)) = if k \in dom f then size (dom f) else (size (dom f)).+1.
proof: Proof. rewrite pcmE /= !umEX /UM.valid /UM.upd /UM.dom. case: (UMC.from f)=>[|f'] //= H; case: decP=>// P _. by case: f' H=>f' F H; rewrite /supp /= !size_map size_ins'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)