proposition: Lemma omapv_mapv (h : Ur) : ocancel f g -> mapv g (omapv f h : Ua) = um_filterv (isSome \o f) h.
proof: Proof. move=>O; rewrite /um_filter omap_comp //=. apply: eq_in_omap; case=>k v H /=. by case X : (f v)=>[a|] //=; rewrite -(O v) X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)