proposition: Lemma In_domX k f : reflect (exists v, (k, v) \In f) (k \in dom f).
proof: Proof. case: dom_find=>[E|v /In_find H E]; constructor; last by exists v. by case=>v /In_find; rewrite E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)