proposition: Lemma kfilt_fcat (p : pred K) (s1 s2 : fmap) : kfilter p (fcat s1 s2) = fcat (kfilter p s1) (kfilter p s2).
proof: Proof. apply/fmapP=>k; rewrite fnd_kfilt !fnd_fcat !fnd_kfilt supp_kfilt mem_filter. by case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)