proposition: Lemma validEb f : reflect (valid f /\ forall k, k \notin dom f) (unitb f).
proof: Proof. case: unitbP=>E; constructor; first by rewrite E valid_unit dom0. case=>V' H; apply: E; move: V' H. rewrite !pcmE /= !umEX /UM.valid /UM.dom /UM.empty -{3}[f]UMC.tfE. case: (UMC.from f)=>[|f' F] // _ H; rewrite !umEX. apply/supp_nilE; case: (supp f') H=>// x s /(_ x). by rewrite inE eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)