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