proposition: Lemma domeq2PtUn (k : K) (v1 : V1) (v2 : V2) (f1 : U1) (f2 : U2) : C1 k = C2 k -> dom_eq2 f1 f2 -> dom_eq2 (pts k v1 \+ f1) (pts k v2 \+ f2).
proof: Proof. move=>E /domeq2P [D1 D2]; apply/domeq2P. set j := (X in X /\ _). have V : j by rewrite /j !validPtUn E D1 D2. by split=>//; apply/dom2E=>x; rewrite !domPtUn !inE V D2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)