proposition: Lemma hcancelPtV2 A x1 x2 (v1 v2 : A) : valid (x1 :-> v1) -> x1 :-> v1 = x2 :-> v2 -> (x1, v1) = (x2, v2).
proof: Proof. by move=>V /(cancelPt2 V) [->] /dyn_inj ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)