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