proposition: Lemma updPtUn k v1 v2 f : upd k v1 (pts k v2 \+ f) = pts k v1 \+ f.
proof: Proof. case V1 : (valid (pts k v2 \+ f)). - by rewrite updUnL domPt inE eq_refl updPt (validPtUn_cond V1). have V2 : valid (pts k v1 \+ f) = false. - by rewrite !validPtUn in V1 *. move/negbT/invalidE: V1=>->; move/negbT/invalidE: V2=>->. by apply: upd_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)