proposition: Lemma umpreim_cond p f k : um_preim p f k -> C k.
proof: Proof. rewrite /um_preim; case E: (find k f)=>[v|] //= _. by move/find_some/dom_cond: E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)