proposition: Lemma umfiltkU p k v f : um_filterk p (upd k v f) = if p k then upd k v (um_filterk p f) else if C k then um_filterk p f else undef.
proof: Proof. rewrite umfiltU /=; case: ifP; case: ifP=>// Hp Hc. - by apply: dom_free; rewrite dom_umfiltk inE Hp. by rewrite upd_condN // Hc. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)