proposition: Lemma omfPtUn f k v h : f (pts k v \+ h) = if valid (pts k v \+ h) then if map_fun f (k, v) is Some v' then pts k v' \+ f h else f h else um_undef.
proof: Proof. by case: f=>s [m X] /=; rewrite !X omapPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)