∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (Φ : CategoryTheory.SmallObject.SuccStruct C)
  (J : Type u_3) [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (x x_1 : J) (f : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj Φ.X₀).map f)
      (CategoryTheory.CategoryStruct.comp (Φ.iterationFunctorObjBotIso J).inv
        ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (Φ.iterationFunctorObjBotIso J).inv
        ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯)))
      ((Φ.iterationFunctor J).map f)