proposition: Lemma umfilt_pred0 f : valid f -> um_filter pred0 f = Unit.
proof: Proof. by move=>W; apply: omap_none. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)