proposition: Lemma oev_rconsE a ks k f z0 : oeval a (rcons ks k) f z0 = if find k f is Some v then a (oeval a ks f z0) k v else oeval a ks f z0.
proof: Proof. by elim: ks z0=>[|k' ks IH] z0 /=. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)