proposition: Lemma dom0E f : valid f -> dom f =i pred0 -> f = Unit.
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.dom /UM.empty -{3}[f]UMC.tfE. case: (UMC.from f)=>[|f' S] //= _; rewrite !umEX fmapE /= {S}. by case: f'; case=>[|kv s] //= P /= /(_ kv.1); 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)