proposition: Lemma In_dom_omap a k f : reflect (exists v w, (k, w) \In f /\ a (k, w) = Some v) (k \in dom (omap a f)).
proof: Proof. case: In_domX=>H; constructor. - by case: H=>v /In_omapX [w H1 H2]; exists v, w. by case=>v [w][X /(In_omap X) Y]; elim: H; exists v. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)