∀ (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_1 : Lean.Server.FileWorker.EditableDocument) (reporterCancelTk_1 : IO.CancelToken)
  (importCachingTask?_1 :
    Option (Lean.Server.ServerTask (Except IO.Error Lean.Server.FileWorker.AvailableImportsCache)))
  (pendingRequests_1 : Lean.Server.FileWorker.PendingRequestMap)
  (rpcSessions_1 : Std.TreeMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare),
  ({ doc := doc, reporterCancelTk := reporterCancelTk, importCachingTask? := importCachingTask?,
        pendingRequests := pendingRequests, rpcSessions := rpcSessions } =
      { doc := doc_1, reporterCancelTk := reporterCancelTk_1, importCachingTask? := importCachingTask?_1,
        pendingRequests := pendingRequests_1, rpcSessions := rpcSessions_1 }) =
    (doc = doc_1 ∧
      reporterCancelTk = reporterCancelTk_1 ∧
        importCachingTask? = importCachingTask?_1 ∧ pendingRequests = pendingRequests_1 ∧ rpcSessions = rpcSessions_1)