(motive : Lean.Server.FileWorker.AvailableImportsCache → Sort u_1) →
  (__discr : Lean.Server.FileWorker.AvailableImportsCache) →
    ((availableImports : ImportCompletion.AvailableImports) →
        (lastRequestTimestampMs : ℕ) →
          motive { availableImports := availableImports, lastRequestTimestampMs := lastRequestTimestampMs }) →
      motive __discr