proposition: Lemma umfiltk_dom_omap V' (U' : union_map_class C V') a (f : U) : um_filterk (mem (dom f)) (omap a f) = omap a f :> U'.
proof: Proof. by rewrite -umfiltk_omap umfiltk_dom'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)