proposition: Lemma evalPtUn a p k v z0 f : valid (pts k v \+ f) -> all (ord k) (dom f) -> eval a p (pts k v \+ f) z0 = eval a p f (if p (k, v) then a z0 k v else z0).
proof: Proof. move=>W /allP H; have: valid (um_filter p (pts k v \+ f)) by rewrite valid_umfilt. rewrite /eval umfiltPtUn W. case: (p (k, v))=>W'; last first. - rewrite oevPtUn //; apply/negP=>/dom_umfilt_subset. by rewrite (negbTE (validPtUnD W)). rewrite domPtUnK //=; last by apply/allP=>x /dom_umfilt_subset /H. by rewrite findPtUn // oevPtUn // (validPtUnD W'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)