proposition: Lemma evalPtUnE v2 v1 a p k (z0 : R) 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 (pts k v1 \+ f) z0 = eval a p (pts k v2 \+ f) z0.
proof: Proof. move=>H; rewrite /eval !oev_dom_umfilt !oev_umfiltA. by rewrite (domPtUnE2 k v1 v2); apply: oevPtUnE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)