proposition: Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) : g ∘ f <$> m = g <$> (f <$> m).
proof: Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
imports: Coq(Permutation) stdpp(options)