proposition: Lemma oevKF a ks f z0 : oeval a ks f z0 = oeval a ks (um_filter (fun x => x.1 \in ks) f) z0.
proof: Proof. elim: ks f z0=>[|k ks IH] f z0 //=. rewrite find_umfilt /= inE eq_refl [in LHS]IH [in RHS]IH /=. congr oeval; last by case: (find k f). by rewrite -umfilt_predI; apply/eq_in_umfilt=>kv /= D; rewrite orKb. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)