proposition: Lemma oev_sub_filter a ks (p : pred K) (h : U) z0 : {subset dom h <= p} -> oeval a (filter p ks) h z0 = oeval a ks h z0.
proof: Proof. move=>S; rewrite oev_filter (eq_in_umfiltI (p2:=predT)) ?umfilt_predT //=. by case=>k v /In_dom /S. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)