proposition: Lemma domeqUn f1 f2 f1' f2' : dom_eq f1 f2 -> dom_eq f1' f2' -> dom_eq (f1 \+ f1') (f2 \+ f2').
proof: Proof. suff L f f' g : dom_eq f f' -> dom_eq (f \+ g) (f' \+ g). - move=>H H'; apply: domeq_trans (L _ _ _ H). by rewrite !(joinC f1); apply: domeq_trans (L _ _ _ H'). move=>F; case/domeqP: (F)=>E H. apply/domeqP; split; first by apply: domeqVUnE F _. move=>x; rewrite !domUn /= inE. by rewrite (domeqVUnE F (domeq_refl g)) H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)