proposition: Lemma omapUnPt a k v f : omap a (f \+ pts k v) = if valid (f \+ pts k v) then if a (k, v) is Some v' then omap a f \+ pts k v' else omap a f else undef.
proof: Proof. rewrite joinC omapPtUn; case: ifP=>// W. by case: (a _)=>// x; rewrite joinC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)