proposition: Lemma omapFE k (f : U) : free f k = omap (fun kv => if kv.1 == k then None else Some kv.2) f.
proof: Proof. case W : (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite free_undef omap_undef. apply: umem_eq. - by rewrite validF. - by rewrite valid_omap. case=>x w; rewrite InF In_omapX /= validF W; split. - by case=>_ /negbTE ->; exists w. by case=>w' H; case: eqP=>// N [<-]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)