proposition: Lemma findPtUn k v f : valid (pts k v \+ f) -> find k (pts k v \+ f) = Some v.
proof: Proof. move=>V'; rewrite findUnL // domPt inE. by rewrite ptsU findU eq_refl valid_unit (validPtUn_cond V'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)