∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (U : CategoryTheory.Comonad C)
  {X : CategoryTheory.Cokleisli U} {Y x : C} (f : (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).obj X ⟶ Y)
  (g : Y ⟶ x),
  (Equiv.refl (U.obj X ⟶ x)) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((Equiv.refl (U.obj X ⟶ Y)) f)
      ((CategoryTheory.Cokleisli.Adjunction.toCokleisli U).map g)