proposition: Lemma cancelPt2 k1 k2 v1 v2 : valid (pts k1 v1 : U) -> pts k1 v1 = pts k2 v2 :> U -> (k1, v1) = (k2, v2).
proof: Proof. move=>H E; have : dom (pts k1 v1 : U) = dom (pts k2 v2 : U) by rewrite E. rewrite !domPtK -(validPt _ v1) -(validPt _ v2) -E H. by case=>E'; rewrite -{k2}E' in E *; rewrite (cancelPt H E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)