proposition: Lemma umfilt_idemp p f : um_filter p (um_filter p f) = um_filter p f.
proof: Proof. rewrite -umfilt_predI; apply/eq_in_umfilt. by case=>k v H /=; rewrite andbb. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)