proposition: Lemma undefbP f : reflect (f = undef) (undefb f).
proof: Proof. rewrite /undef /= !umEX /UM.undefb -{1}[f]UMC.tfE. by case: (UMC.from f)=>[|f' F]; constructor; rewrite !umEX. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)