proposition: Lemma omapPt a k v : omap a (pts k v) = if C k then if a (k, v) is Some w then pts k w else Unit else undef.
proof: Proof. rewrite /omap validPt assocsPt; case C': (C k)=>//=. by case: (a (k, v))=>// x; rewrite unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)