proposition: Lemma dom_omap_sub a f : {subset dom (omap a f) <= dom f}.
proof: Proof. elim/um_indf: f=>[||k v f IH W P] x. - by rewrite omap_undef dom_undef. - by rewrite omap0 dom0. rewrite omapPtUn W domPtUn W !inE /=. case E : (a _)=>[b|]; last by move/IH=>->; rewrite orbT. rewrite domPtUn inE; case/andP=>W2. by case/orP=>[->//|/IH ->]; rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)