proposition: Lemma dom_umfiltE p f : dom (um_filter p f) = filter (fun k => if find k f is Some v then p (k, v) else false) (dom f).
proof: Proof. apply: ord_sorted_eq=>//=. - by apply: sorted_filter; [apply: trans | apply: sorted_dom]. move=>k; rewrite mem_filter; apply/idP/idP. - by case/dom_umfilt=>w [H1 H2]; move/In_find: H2 (H2) H1=>-> /In_dom ->->. case X: (find k f)=>[v|] // /andP [H1 _]; move/In_find: X=>H2. by apply/dom_umfilt; exists v. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)