proposition: Lemma domeqK f1 f2 f1' f2' : valid (f1 \+ f1') -> dom_eq (f1 \+ f1') (f2 \+ f2') -> dom_eq f1 f2 -> dom_eq f1' f2'.
proof: Proof. move=>V1 /domeqP [E1 H1] /domeqP [E2 H2]; move: (V1); rewrite E1=>V2. apply/domeqP; split; first by rewrite (validE2 V1) (validE2 V2). by apply: domK V1 V2 H1 H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)