proposition: Lemma umfiltkF p k f : um_filterk p (free f k) = if p k then free (um_filterk p f) k else um_filterk p f.
proof: Proof. rewrite umfiltF; case: ifP=>// N. by rewrite dom_free // dom_umfiltk inE N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)