proposition: Lemma map_functorial : forall A B C (f : A -> B) (g : B -> C) (m : M A), g <$> (f <$> m) = (fun x => g (f x)) <$> m.
proof: Proof. intros ; cbv. rewrite monad_law3. f_equal. extensionality a. rewrite monad_law1. reflexivity. Qed.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)