proposition: Lemma dom_omap_umfilt V' (U' : union_map_class C V') a f : dom (omap a f : U') = dom (um_filter (isSome \o a) f).
proof: Proof. apply/domE=>x; apply/idP/idP. - case/In_dom_omap=>// v [w][H1 H2]. by apply/dom_umfilt; exists w; rewrite /= H2. case/dom_umfilt=>w [/= H1 H2]; case E : (a _) H1=>[xa|//] _. by apply/In_dom_omap=>//; exists xa, w. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)