proposition: Lemma oev_umfiltA a ks p f z0 : oeval a ks (um_filter p f) z0 = oeval (fun r k v => if p (k, v) then a r k v else r) ks f z0.
proof: Proof. elim: ks z0=>[|k ks IH] z0 //=; rewrite IH find_umfilt. by case E : (find k f)=>[b|] //; case: ifP=>//. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)