proposition: Lemma kfilter_predU p1 p2 (s : fmap) : kfilter (predU p1 p2) s = fcat (kfilter p1 s) (kfilter p2 s).
proof: Proof. apply/fmapP=>k; rewrite fnd_kfilt fnd_fcat !fnd_kfilt supp_kfilt mem_filter. rewrite inE /=; case: (ifP (p1 k)); case: (ifP (p2 k))=>//=; by [case: ifP | case: suppP]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)