proposition: Lemma dom_umfilt p f k : reflect (exists v, [/\ p (k, v) & (k, v) \In f]) (k \in dom (um_filter p f)).
proof: Proof. case: In_domX=>H; constructor. - by case: H=>v /In_umfilt []; exists v. by case=>v [Hp Hf]; elim: H; exists v; apply/In_umfilt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)