proposition: Lemma umfilt_mem0L p f : valid f -> (forall k v, (k, v) \In f -> ~~ p (k, v)) -> um_filter p f = Unit.
proof: Proof. rewrite /um_filter => VF H. apply: omap_none => //. by case=> k v I; rewrite (negbTE (H k v I)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)