proposition: Lemma evalUEU 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 (upd k v1 f) z0 = eval a p (upd k v2 f) z0.
proof: Proof. move=>H; rewrite /eval !oev_dom_umfilt !oev_umfiltA. rewrite (oevUE _ _ _ H); apply: eq_in_oevK; congr filter. by apply/domE=>x; rewrite !domU. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)