proposition: Lemma umfiltk_omap V' (U' : union_map_class C V') a p f : omap a (um_filterk p f) = um_filterk p (omap a f) :> U'.
proof: Proof. rewrite /um_filter !omap_comp //= /obind/oapp /=. by apply: eq_in_omap; case=>k v /=; case: ifP; case: a. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)