proposition: Lemma findPtUn2 k1 k2 v f : valid (pts k2 v \+ f) -> find k1 (pts k2 v \+ f) = if k1 == k2 then Some v else find k1 f.
proof: Proof. move=>V'; rewrite findUnL // domPt inE eq_sym. by rewrite findPt2 (validPtUn_cond V') andbT /=; case: ifP=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)