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