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