∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {F₀ F₁ F₂ : CategoryTheory.Functor C C} (α : F₀ ⟶ F₁)
  (β : F₁ ⟶ F₂) (X : CategoryTheory.Endofunctor.Coalgebra F₀),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans (CategoryTheory.CategoryStruct.comp α β)).obj X).str
      (F₂.map
        (CategoryTheory.Iso.refl
            ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans (CategoryTheory.CategoryStruct.comp α β)).obj
                X).V).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans (CategoryTheory.CategoryStruct.comp α β)).obj
              X).V).hom
      (((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).comp
              (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans β)).obj
          X).str