proposition: Lemma joinKf f1 f2 f : valid (f1 \+ f) -> f1 \+ f = f2 \+ f -> f1 = f2.
proof: Proof. rewrite -{3}[f1]UMC.tfE -{2}[f2]UMC.tfE !pcmE /= !umEX /UM.valid /UM.union. case: (UMC.from f) (UMC.from f1) (UMC.from f2)=> [|f' H]; case=>[|f1' H1]; case=>[|f2' H2] //; case: ifP=>//; case: ifP=>// D1 D2 _ E. by apply: fcatsK E; rewrite D1 D2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)