proposition: Lemma oev_filter a ks (p : pred K) f z0 : oeval a (filter p ks) f z0 = oeval a ks (um_filterk p f) z0.
proof: Proof. rewrite oev_umfilt oevFK -filter_predI; congr oeval. by apply: eq_in_filter=>k D /=; case: dom_find=>[->|v ->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)