proposition: Lemma umfiltUnPt p k v f : um_filter p (f \+ pts k v) = if valid (f \+ pts k v) then if p (k, v) then um_filter p f \+ pts k v else um_filter p f else undef.
proof: Proof. by rewrite /um_filter omapUnPt; 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)