proposition: Lemma cancelPt k v1 v2 : valid (pts k v1 : U) -> pts k v1 = pts k v2 :> U -> v1 = v2.
proof: Proof. by rewrite validPt !ptsU; apply: upd_inj. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)