proposition: Lemma oevKA a ks f z0 : oeval a ks f z0 = oeval (fun r k v => if k \in ks then a r k v else r) ks f z0.
proof: Proof. elim: ks a z0=>[|k ks IH] a z0 //=; rewrite inE eq_refl [in LHS]IH [in RHS]IH. by apply: eq_in_oevA=>r k' v; case: ifP=>// D; rewrite inE D orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)