proposition: Lemma eq_in_oevA a1 a2 ks f z0 : (forall r k v, a1 r k v = a2 r k v) -> oeval a1 ks f z0 = oeval a2 ks f z0.
proof: Proof. move=>H; elim: ks z0=>[|k ks IH] z0 //=. by case E : (find k f)=>[b|] //; rewrite IH H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)