proposition: Lemma In_omapX a k v f : (k, v) \In omap a f <-> exists2 w, (k, w) \In f & a (k, w) = Some v.
proof: Proof. rewrite In_omap_raw; split; first by case=>w []; exists w. case=>w H X; exists w; split=>//. - by move/In_dom/dom_cond: H. by rewrite valid_omap //; move/In_dom/dom_valid: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)