∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] {G : CategoryTheory.Functor C D},
  autoParam (∀ (j : J), Order.IsSuccLimit j → CategoryTheory.Limits.PreservesColimitsOfShape (↑(Set.Iio j)) G)
      CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape._autoParam →
    CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G