proposition: Lemma subdom_umfiltkE p f : {subset dom f <= p} <-> um_filterk p f = f.
proof: Proof. split; last by move=><- a; rewrite dom_umfiltk; case/andP. by move/eq_in_umfiltk=>->; rewrite umfilt_predT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)