proposition: Lemma unitL f : unit \+ f = f.
proof: Proof. rewrite -[f]UMC.tfE !umEX /UM.union /UM.empty. by case: (UMC.from f)=>[//|f' H]; rewrite disjC disj_nil fcat0s. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)