proposition: Lemma oevPtUnE a k ks v1 v2 f z0 : (forall r, a r k v1 = a r k v2) -> oeval a ks (pts k v1 \+ f) z0 = oeval a ks (pts k v2 \+ f) z0.
proof: Proof. move=>H; case W1 : (valid (pts k v1 \+ f)); last first. - have W2 : valid (pts k v2 \+ f) = false by rewrite !validPtUn in W1 *. move/invalidE: (negbT W1)=>->; move/invalidE: (negbT W2)=>->. by rewrite oev_undef. elim: ks z0=>[|k' ks IH] z0 //=. have W2 : valid (pts k v2 \+ f) by rewrite !validPtUn in W1 *. by rewrite !findPtUn2 //; case: eqP=>// ->; rewrite H; apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)