proposition: Lemma In_omap_raw a k v f : (k, v) \In omap a f <-> exists w, [/\ C k, valid (omap a f), (k, w) \In f & a (k, w) = Some v].
proof: Proof. elim/um_indf: f k v=>[||x w f IH W P] k v. - by rewrite omap_undef; split=>[/In_undef|[w][]] //; rewrite valid_undef. - by rewrite omap0; split=>[/In0|[w][??] /In0]. split=>[H|[w1][C' V1 H E]]. - move: (dom_valid (In_dom H)); rewrite omapPtUn W in H *. case E: (a (x, w)) H=>[z|] H W1; last first. - by case/IH: H=>w1 []; exists w1; split=>//; apply/InR. move: H; rewrite InPtUnE //. case; first by case=>->->; exists w; rewrite (validPtUn_cond W1). by case/IH=>w1 []; exists w1; split=>//; apply/InR. rewrite omapPtUn W in V1 *; move/(InPtUnE _ W): H=>H. case: H E V1; first by case=>->->-> V1; apply/InPtUnE=>//; left. case: (a (x, w))=>[b|] H E V1; last by apply/IH; exists w1. by rewrite InPtUnE //; right; apply/IH; exists w1; rewrite (validR V1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)