proposition: Lemma assocs_umfilt p f : assocs (um_filter p f) = filter p (assocs f).
proof: Proof. elim/um_indf: f=>[||k v f IH W /(order_path_min (@trans K)) P]. - by rewrite umfilt_undef assocs_undef. - by rewrite umfilt0 assocs0. rewrite umfiltPtUn W assocsPtUn //=. case: ifP W=>// H W; rewrite assocsPtUn; first by rewrite IH. - suff: valid (um_filter p (pts k v \+ f)) by rewrite umfiltPtUn W H. by rewrite valid_umfilt. by apply/allP=>x; move/allP: P=>P; move/dom_umfilt_subset/P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)