s d (m : morphism C s d) : CO d o F _1 m = G _1 m o CO s. Proof. case HM. case HO. exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core.