proposition: Lemma umfiltv_predD (q1 q2 : pred V) f : subpred q1 q2 -> um_filterv q2 f = um_filterv q1 f \+ um_filterv (predD q2 q1) f.
proof: Proof. by move=>H; apply: umfilt_predD; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)