proposition: Lemma dom_umfiltk p f : dom (um_filterk p f) =i predI p (mem (dom f)).
proof: Proof. by move=>k; rewrite dom_umfiltkE mem_filter. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)