proposition: Lemma omap_none (a : K * V -> option V') (f : U) : valid f -> (forall kv, kv \In f -> a kv = None) -> omap a f = Unit :> U'.
proof: Proof. move=>W /eq_in_omap ->. elim/um_indf: f W=>[||k v f IH W P]; rewrite ?valid_undef ?omap0 // => _. by rewrite omapPtUn W IH // (validR W). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)