proposition: Lemma evalFPtUn k v z0 f : valid (pts k v \+ f) -> eval a p (pts k v \+ f) z0 = if p (k, v) then a Unit k v \+ eval a p f z0 else eval a p f z0.
proof: Proof. move=>W; rewrite /eval umfiltPtUn W. have D : k \notin dom f by apply: (validPtUnD W). have Ck : C k by apply: (validPtUn_cond W). case: ifP=>_; last by apply: oevPtUn_sub=>//; apply: dom_umfilt_subset. rewrite oevUn // -(oev_sub_filter (p:=mem [:: k])) ?(domPtK,Ck) //. rewrite -dom_umfiltkE umfiltPtUn /= valid_umfiltUnR // inE eq_refl. rewrite umfilt_mem0L ?(inE,valid_umfilt,validR W) //=; first last. - by move=>?? /In_umfilt [] _ /In_dom Df; rewrite inE; case: eqP Df D=>// ->->. rewrite unitR domPtK Ck /= findPt Ck -frame unitL. rewrite -(oev_sub_filter (p:=mem (dom f))) //. rewrite -dom_umfiltkE umfiltPtUn /= valid_umfiltUnR // (negbTE D). congr (a (oeval a (dom _) f z0) k v). by rewrite -subdom_umfiltkE; apply: dom_umfilt_subset. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)