proposition: Lemma omap_some (a : K * V -> option V) (f : U) : (forall kv, kv \In f -> a kv = Some kv.2) -> omap a f = f.
proof: Proof. by move/eq_in_omap=>->; apply: mapv_id. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)