proposition: Lemma domeq2Pt (k : K) (v1 : V1) (v2 : V2) : C1 k = C2 k -> dom_eq2 (pts k v1 : U1) (pts k v2 : U2).
proof: Proof. by move=>E; apply/domeq2P; rewrite !validPt !domPtK E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)