proposition: Lemma dom_umfilt2 p1 p2 f x : x \in dom (um_filter p1 (um_filter p2 f)) = (x \in dom (um_filter p1 f)) && (x \in dom (um_filter p2 f)).
proof: Proof. rewrite -umfilt_predI; apply/idP/idP. - case/dom_umfilt=>v [/andP [X1 X2] H]. by apply/andP; split; apply/dom_umfilt; exists v. case/andP=>/dom_umfilt [v1][X1 H1] /dom_umfilt [v2][X2 H2]. move: (In_fun H1 H2)=>E; rewrite -{v2}E in X2 H2 *. by apply/dom_umfilt; exists v1; split=>//; apply/andP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)