∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) {j : J} (iter : Φ.Iteration j)
  (hj : i₂ ≤ j),
  CategoryTheory.Arrow.mk ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE h₁₂)) =
    CategoryTheory.Arrow.mk (iter.F.map (CategoryTheory.homOfLE h₁₂))