∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J}
  (iter iter_1 : Φ.Iteration j), iter = iter_1 → ∀ {j' : J} (hj' : j' ≤ j), iter.trunc hj' = iter_1.trunc hj'