proposition: Lemma oevUE a k ks v1 v2 f (z0 : R) : (forall r, a r k v1 = a r k v2) -> oeval a ks (upd k v1 f) z0 = oeval a ks (upd k v2 f) z0.
proof: Proof. move=>H; elim: ks z0=>[|k' ks IH] z0 //=. rewrite !findU; case: eqP=>// ->; rewrite IH. by congr oeval; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)