{α : Type} →
  {P : Sort u} →
    {response response' : α} →
      Lean.Server.ServerRequestResponse.success response = Lean.Server.ServerRequestResponse.success response' →
        (response ≍ response' → P) → P