proposition: Lemma domeqUnf f f1 f2 f1' f2' : dom_eq f1 (f \+ f2) -> dom_eq (f \+ f1') f2' -> dom_eq (f1 \+ f1') (f2 \+ f2').
proof: Proof. by move=>D1 D2; rewrite (joinC f1) (joinC f2); apply: domeqfUn D2 D1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)