proposition: Lemma oevPtUn a k ks v z0 f : valid (pts k v \+ f) -> k \notin ks -> oeval a ks (pts k v \+ f) z0 = oeval a ks f z0.
proof: Proof. move=>W S; apply: eq_in_oevF=>k0 v0 H. rewrite InPtUnE //; split; last by right. by case=>// [][??]; subst k0; rewrite H in S. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)