proposition: Lemma subdom_umfiltk0 p f : valid f -> {subset dom f <= predC p} <-> um_filterk p f = Unit.
proof: Proof. move=>W; split=>H. - by rewrite (eq_in_umfiltk (p2:=pred0)) ?umfilt_pred0 // => a /H /negbTE ->. move=>k X; case: dom_find X H=>// a _ -> _; rewrite umfiltU !inE /=. case: (ifP (p k)) =>// _ /unitbE. by case: ifP; [rewrite um_unitbU | rewrite unitb_undef]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)