∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (hX hX_1 : CategoryTheory.Limits.IsTerminal X),
  hX = hX_1 →
    ∀ (F : CategoryTheory.Functor J C) [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
      CategoryTheory.Limits.coneOfDiagramTerminal hX F = CategoryTheory.Limits.coneOfDiagramTerminal hX_1 F