proposition: Lemma findUnPt2 k1 k2 v f : valid (f \+ pts k2 v) -> find k1 (f \+ pts k2 v) = if k1 == k2 then Some v else find k1 f.
proof: Proof. by rewrite joinC; apply: findPtUn2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)