∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x y : CategoryTheory.Limits.limit F),
  (∀ (j : J), CategoryTheory.Limits.limit.π F j x = CategoryTheory.Limits.limit.π F j y) → x = y