proposition: Lemma validU k v f : valid (upd k v f) = C k && valid f.
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.upd. case: (UMC.from f)=>[|f' F]; first by rewrite andbF. by case: decP=>[|/(introF idP)] ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)