proposition: Lemma freeUn k f1 f2 : free (f1 \+ f2) k = if k \in dom (f1 \+ f2) then free f1 k \+ free f2 k else f1 \+ f2.
proof: Proof. rewrite !pcmE /= !umEX /UM.free /UM.union /UM.dom. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] //. case: ifP=>// E1; rewrite supp_fcat inE /=. case: ifP=>E2; last by rewrite !umEX rem_supp // supp_fcat inE E2. rewrite disj_rem; last by rewrite disjC disj_rem // disjC. rewrite !umEX; case/orP: E2=>E2. - suff E3: k \notin supp f2' by rewrite -fcat_rems // (rem_supp E3). by case: disjP E1 E2=>// H _; move/H. suff E3: k \notin supp f1' by rewrite -fcat_srem // (rem_supp E3). by case: disjP E1 E2=>// H _; move/contra: (H k); rewrite negbK. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)