proposition: Lemma omap_noneR (a : K * V -> option V') (f : U) : omap a f = Unit :> U' -> forall kv, kv \In f -> a kv = None.
proof: Proof. elim/um_indf: f=>[H|H|k v f IH W P O] kv. - by move/In_undef. - by move/In0. move: O; rewrite omapPtUn W. case E: (a (k, v)). - by move=>/unitbP; rewrite um_unitbPtUn. move=>O /InUn [/InPt [->]|] //. by apply: IH =>//; move: W; rewrite validPtUn; case/and3P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)