s d (m : morphism C s d) : (F o G') _1 m o F _1 (T s) = F _1 (T d) o (F o G) _1 m := ((composition_of F _ _ _ _ _)^) @ (ap (fun m => F _1 m) (commutes_sym T _ _ _)) @ (composition_of F _ _ _ _ _).
Require Import Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core.