fact: Definition Mem_UmMap f := fun x : K * V => valid f /\ [pcm pts x.1 x.2 <= f].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)