{P : Sort u} →
  {doc : Lean.Server.FileWorker.EditableDocument} →
    {reporterCancelTk : IO.CancelToken} →
      {importCachingTask? :
          Option (Lean.Server.ServerTask (Except IO.Error Lean.Server.FileWorker.AvailableImportsCache))} →
        {pendingRequests : Lean.Server.FileWorker.PendingRequestMap} →
          {rpcSessions : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare} →
            {doc' : Lean.Server.FileWorker.EditableDocument} →
              {reporterCancelTk' : IO.CancelToken} →
                {importCachingTask?' :
                    Option (Lean.Server.ServerTask (Except IO.Error Lean.Server.FileWorker.AvailableImportsCache))} →
                  {pendingRequests' : Lean.Server.FileWorker.PendingRequestMap} →
                    {rpcSessions' : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare} →
                      { doc := doc, reporterCancelTk := reporterCancelTk, importCachingTask? := importCachingTask?,
                            pendingRequests := pendingRequests, rpcSessions := rpcSessions } =
                          { doc := doc', reporterCancelTk := reporterCancelTk',
                            importCachingTask? := importCachingTask?', pendingRequests := pendingRequests',
                            rpcSessions := rpcSessions' } →
                        (doc = doc' →
                            reporterCancelTk = reporterCancelTk' →
                              importCachingTask? = importCachingTask?' →
                                pendingRequests = pendingRequests' → rpcSessions = rpcSessions' → P) →
                          P