proposition: Lemma find_omap a k f : find k (omap a f) = if find k f is Some v then a (k, v) else None.
proof: Proof. case E1 : (find k (omap a f))=>[b|]. - by move/In_find: E1=>/In_omapX [] // x /In_find ->. move/find_none/negP: E1=>E1. case E2 : (find k f)=>[c|] //; move/In_find: E2=>E2. case E3: (a (k, c))=>[d|] //; elim: E1. by apply/In_dom_omap=>//; exists d, c. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)