proposition: Lemma eq_in_omap a1 a2 f : (forall kv, kv \In f -> a1 kv = a2 kv) -> omap a1 f = omap a2 f.
proof: Proof. elim/um_indf: f=>[||k v f IH W P H]; rewrite ?omap_undef ?omap0 //. rewrite !omapPtUn W; move/H: (InPtUnL W)=>->. by case E2: (a2 _)=>[b2|]; (rewrite IH; last by move=>kv /(InR W)/H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)