proposition: Lemma all_supp_kfilterP q : all C (supp f) -> all C (supp (kfilter q f)).
proof: Proof. move=>H; apply/allP=>x; rewrite supp_kfilt mem_filter. by case/andP=>_ /(allP H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)