∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {F : CategoryTheory.Functor C C}
  (V : CategoryTheory.Endofunctor.Coalgebra F),
  CategoryTheory.CategoryStruct.comp V.str (F.map (CategoryTheory.CategoryStruct.id V.V)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id V.V) V.str