proposition: Lemma umpreim_dom f : um_preim predT f =1 mem (dom f).
proof: Proof. move=>x; rewrite /um_preim /=. case X: (find x f)=>[a|] /=; first by rewrite (find_some X). by apply/esym/negbTE/find_none. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)