proposition: Lemma findPt_inv k1 k2 v w : find k1 (pts k2 v : U) = Some w -> [/\ k1 = k2, v = w & C k2].
proof: Proof. rewrite ptsU findU; case: eqP; last by case: ifP=>//; rewrite find0E. by move=>->; rewrite valid_unit 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)