proposition: Lemma umfiltPt p k v : um_filter p (pts k v) = if C k then if p (k, v) then pts k v else Unit else undef.
proof: Proof. by rewrite /um_filter omapPt; case: (ifP (p (k, v))). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)