∀ {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 : J) {j : J} (iter : Φ.Iteration j) (hi : i ≤ j),
  (Φ.iterationFunctor J).obj i = iter.F.obj ⟨i, hi⟩