proposition: Lemma valid_umfiltkUn p1 p2 f : valid f -> {in dom f, forall x, x \in p1 -> x \in p2 -> false} -> valid (um_filterk p1 f \+ um_filterk p2 f).
proof: Proof. move=>W H; rewrite validUnAE !valid_umfilt W /=. apply/allP=>x; case/dom_umfilt=>v1 /= [H2 F1]. apply/negP; case/dom_umfilt=>v2 /= [H1 F2]. by move: (H x (In_dom F1) H1 H2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)