proposition: Lemma umfiltkPt p k v : um_filterk p (pts k v : U) = if p k then pts k v else if C k then Unit else undef.
proof: Proof. rewrite ptsU umfiltU umfilt0 free0 /=. by case: ifP=>//; move/negbT=>N; rewrite upd_condN // if_same. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)