proposition: Lemma findPt2 k1 k2 v : find k1 (pts k2 v : U) = if (k1 == k2) && C k2 then Some v else None.
proof: Proof. by rewrite ptsU findU valid_unit andbT find0E; case: ifP=>//=; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)