proposition: Lemma empbP f : reflect (f = Unit) (empb f).
proof: Proof. rewrite pcmE /= !umEX /UM.empty /UM.empb -{1}[f]UMC.tfE. case: (UMC.from f)=>[|f' F]; first by apply: ReflectF; rewrite !umEX. case: eqP=>E; constructor; rewrite !umEX. - by move/supp_nilE: E=>->. by move=>H; rewrite H in E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)