proposition: Lemma umpleq_filtk_meet a p f : {subset dom a <= p} -> [pcm a <= f] -> [pcm a <= um_filterk p f].
proof: Proof. by move=>D /(umfilt_pleq_mono (p \o fst)); rewrite (eq_in_umfiltk D) umfilt_predT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)