proposition: Lemma joinCA f1 f2 f3 : f1 \+ (f2 \+ f3) = f2 \+ (f1 \+ f3).
proof: Proof. rewrite !umEX /UM.union /=. case: (UMC.from f1) (UMC.from f2) (UMC.from f3)=>[|f1' H1][|f2' H2][|f3' H3] //. case E1: (disj f2' f3'); last first. - by case E2: (disj f1' f3')=>//; rewrite disj_fcat E1 andbF. rewrite disj_fcat andbC. case E2: (disj f1' f3')=>//; rewrite disj_fcat (disjC f2') E1 /= andbT. by case E3: (disj f1' f2')=>//; rewrite fcatAC // E1 E2 E3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)