proposition: Lemma valid_omapPtUn a k v f : [&& C k, valid f & k \notin dom f] -> valid (pts k v \+ omap a f).
proof: Proof. move/and3P => [H1 H2 H3]. rewrite validPtUn H1 valid_omap // H2 /=. by apply: contra H3; apply: dom_omap_sub. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)