proposition: Corollary umfiltk_dom' f : um_filterk (mem (dom f)) f = f.
proof: Proof. case/boolP: (valid f)=>H. - by rewrite -{2}[f]unitR umfiltk_dom // unitR. move/invalidE: H=>->; apply: umfilt_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)