proposition: Lemma domeqPtUn k v1 v2 f1 f2 : dom_eq f1 f2 -> dom_eq (pts k v1 \+ f1) (pts k v2 \+ f2).
proof: Proof. by apply: domeqUn=>//; apply: domeqPt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)