∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type v} [Finite α]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) (CategoryTheory.Ind C)