proposition: Lemma eq_in_omapE a1 a2 f : (forall kv, kv \In f -> a1 kv = a2 kv) <-> omap a1 f = omap a2 f.
proof: Proof. split; first by apply: eq_in_omap. elim/um_indf: f=>[||k v f IH W P H]. - by move=>_ kv /In_undef. - by move=>E kv /In0. move=>kv /(InPtUnE _ W) [->|]. - have : find k (omap a1 (pts k v \+ f)) = find k (omap a2 (pts k v \+ f)) by rewrite H. - by rewrite !find_omap // findPtUn. apply: {kv} IH; apply: eq_in_omap; case=>k1 v1 X. have : find k1 (omap a1 (pts k v \+ f)) = find k1 (omap a2 (pts k v \+ f)) by rewrite H. rewrite !find_omap // findPtUn2 //. case: eqP X=>[-> /In_dom|_ /In_find -> //]. by move/negbTE: (validPtUnD W)=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)