proposition: Lemma map_fmap_map_compose `{FinMap A MA, FinMap B MB} {C1 C2} (f : C1 → C2) (m : MB C1) (n : MA B) : f <$> (m ∘ₘ n) = (f <$> m) ∘ₘ n.
proof: Proof. apply map_eq; intros a. rewrite lookup_fmap, !map_lookup_compose. destruct (n !! a); simpl; [|done]. by rewrite lookup_fmap. Qed.
imports: Coq(Permutation) stdpp(options)