proposition: Lemma umPtPtE (k1 k2 : K) (v1 v2 : V) : (k1 \\-> v1 == k2 \\-> v2) = (k1 == k2) && (v1 == v2).
proof: Proof. rewrite {1}/eq_op /= /UnionMapEq.unionmap_eq /um_pts !umEX /=. by rewrite {1}/eq_op /= /feq eqseq_cons andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)