proposition: Lemma mapv_id (f : U) : mapv id f = f.
proof: Proof. elim/um_indf: f=>[||k v f IH W P]. - by rewrite omap_undef. - by rewrite omap0. by rewrite omapPtUn W /= IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)