proposition: Lemma umfiltU p k v f : um_filter p (upd k v f) = if C k then if p (k, v) then upd k v (um_filter p f) else free (um_filter p f) k else undef.
proof: Proof. by rewrite /um_filter omapU //; case: (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)