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