proposition: Lemma omap_comp (f : U1) : omap a2 (omap a1 f : U2) = omap (fun x => obind (fun v => a2 (x.1, v)) (a1 x)) f :> U3.
proof: Proof. elim/um_indf: f=>[||k v f IH W P]; rewrite ?omap_undef ?omap0 //. rewrite !omapPtUn W; case: (a1 (k, v))=>[w|//]. rewrite omapPtUn validPtUn (validPtUn_cond W) valid_omap // (validR W) IH. by rewrite (contra _ (validPtUnD W)) //; apply: dom_omap_sub. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)