proposition: Lemma dom_omap_some (a : K * V -> option V') f : (forall x, x \In f -> a x) -> dom (omap a f) = dom f.
proof: Proof. move=>H; apply/domE=>k; apply/idP/idP=>/In_domX [w]. - by case/In_omapX => v /In_dom. move/[dup]/H; case A: (a (k, w))=>[v|] // _ {}H. suff : (k, v) \In omap a f by apply: In_dom. by apply/In_omapX=>//; exists w. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)