proposition: Lemma all_supp_mapfP (a : K -> V -> V) : all C (supp f) -> all C (supp (mapf a f)).
proof: Proof. by move=>H; apply/allP=>x; rewrite supp_mapf; move/(allP H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)