proposition: Lemma umfilt_predI p1 p2 f : um_filter (predI p1 p2) f = um_filter p1 (um_filter p2 f).
proof: Proof. rewrite /um_filter omap_comp; apply: eq_in_omap; case=>k v H /=. by case: (ifP (p2 (k, v))); rewrite ?andbT ?andbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)