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