proposition: Lemma evalPt a p (z0 : R) k v : eval a p (pts k v) z0 = if C k && p (k, v) then a z0 k v else z0.
proof: Proof. rewrite /eval umfiltPt. case E1: (C k); last by rewrite dom_undef oev_nil. case: (p (k, v)); last by rewrite dom0 oev_nil. by rewrite domPtK E1 /= findPt E1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)