proposition: Lemma oev_dom_umfilt a p f z0 : oeval a (dom (um_filter p f)) f z0 = oeval a (dom f) (um_filter p f) z0.
proof: Proof. rewrite dom_umfiltE oev_filter; apply: eq_in_oevF=>k v _. by rewrite !In_umfilt /=; split; case=>H Y; move/In_find: Y (Y) H=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)