proposition: Lemma dom_umfiltkE p f : dom (um_filterk p f) = filter p (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=>v [/= -> /In_dom]. by case/andP=>H1 /In_domX [v H2]; 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)