proposition: Lemma hcancelPtT2 A1 A2 x1 x2 (v1 : A1) (v2 : A2) : valid (x1 :-> v1) -> x1 :-> v1 = x2 :-> v2 -> (x1, A1) = (x2, A2).
proof: Proof. by move=>V; case/(cancelPt2 V)=>-> E _; rewrite E. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)