proposition: Lemma oev_consP a k v ks f z0 : (k, v) \In f -> oeval a (k :: ks) f z0 = oeval a ks f (a z0 k v).
proof: Proof. by move/In_find=>/= ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)