proposition: Lemma oevU a k ks v1 v2 f z0 : (k, v2) \In f -> (forall r, a r k v1 = a r k v2) -> oeval a ks (upd k v1 f) z0 = oeval a ks f z0.
proof: Proof. move=>X H. have [C' W] : C k /\ valid f by move/In_dom/dom_cond: (X); case: (X). rewrite [in RHS](_ : f = upd k v2 f); first by apply: oevUE. apply: umem_eq=>//; first by rewrite validU C' W. case=>k' v'; rewrite InU validU C' W /=. case: ifP=>[/eqP ->|_]; last by split=>//; case. by split=>[/(In_fun X)|[_] ->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)