proposition: Lemma domPtK k v : dom (pts k v : U) = if C k then [:: k] else [::].
proof: Proof. rewrite !umEX /= /UM.dom /supp /UM.pts /UM.upd /UM.empty /=. by case D : (decP _)=>[a|a] /=; rewrite ?a ?(introF idP a). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)