proposition: Lemma In_umfilt x p f : x \In um_filter p f <-> p x /\ x \In f.
proof: Proof. case: x => k v; rewrite In_omapX; split=>[[w H]|[I H]]. - by case E: (p (k, w))=>//=; case=><-. by exists v=>//; rewrite I. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)