{P : Sort u_1} →
  {diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
    {cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite)} →
      {isLimit : CategoryTheory.Limits.IsLimit cone} →
        {diagram' : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
          {cone' : CategoryTheory.Limits.Cone (diagram'.comp FintypeCat.toProfinite)} →
            {isLimit' : CategoryTheory.Limits.IsLimit cone'} →
              { diagram := diagram, cone := cone, isLimit := isLimit } =
                  { diagram := diagram', cone := cone', isLimit := isLimit' } →
                (diagram = diagram' → cone ≍ cone' → isLimit ≍ isLimit' → P) → P