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