∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t)
  (x₁ x₂ : t.pt), ∃ j x₁' x₂', t.ι.app j x₁' = x₁ ∧ t.ι.app j x₂' = x₂