proposition: Lemma map_comp m: mapk g (@mapk A B V f m) = mapk (comp g f) m.
proof: Proof. elim/fmap_ind': m =>//= k v s P IH. rewrite [mapk (g \o f) _]mapk_ins //. rewrite mapk_ins // mapk_ins //; first by rewrite IH. exact: (path_mapk Hf P). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)