proposition: Lemma assocsPt k v : assocs (pts k v : U) = if C k then [:: (k, v)] else [::].
proof: Proof. rewrite !umEX /UM.assocs/UM.pts /=. by case E: decP=>[a|a] /=; [rewrite a | case: ifP]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)