proposition: Lemma omapPtUn a k v f : omap a (pts k v \+ f) = if valid (pts k v \+ f) then if a (k, v) is Some v' then pts k v' \+ omap a f else omap a f else undef.
proof: Proof. case: ifP=>X; last first. - by move/invalidE: (negbT X)=>->; rewrite omap_undef. rewrite omapUn // omapPt (validPtUn_cond X). by case: (a _)=>//; rewrite unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)