proposition: Lemma umfilt_mem0 p f : um_filter p f = Unit -> forall k v, (k, v) \In f -> ~~ p (k, v).
proof: Proof. rewrite /um_filter => H k v I. have: ((if p (k, v) then Some v else None) = None). - by apply: (omap_noneR H). by case: (p (k, v)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)