proposition: Lemma findU k1 k2 v f : find k1 (upd k2 v f) = if k1 == k2 then if C k2 && valid f then Some v else None else if C k2 then find k1 f else None.
proof: Proof. rewrite pcmE /= !umEX /UM.valid /UM.find /UM.upd. case: (UMC.from f)=>[|f' F]; first by rewrite andbF !if_same. case: decP=>H; first by rewrite H /= fnd_ins. by rewrite (introF idP H) /= if_same. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)