proposition: Lemma valid_omap a f : valid (omap a f) = valid f.
proof: Proof. elim/um_indf: f=>[||k v f IH W P]. - by rewrite omap_undef !valid_undef. - by rewrite omap0 !valid_unit. rewrite omapPtUn W; case X : (a _)=>[b|]; last by rewrite IH (validR W). rewrite validPtUn (validPtUn_cond W) IH (validR W). by apply: contra (notin_path P); 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)