proposition: Lemma joinC f1 f2 : f1 \+ f2 = f2 \+ f1.
proof: Proof. rewrite !umEX /UM.union. case: (UMC.from f1)=>[|f1' H1]; case: (UMC.from f2)=>[|f2' H2] //. by case: ifP=>E; rewrite disjC E // fcatC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)