(motive : Except String ImportCompletion.AvailableImports → Sort u_1) →
  (x : Except String ImportCompletion.AvailableImports) →
    ((availableImports : ImportCompletion.AvailableImports) → motive (Except.ok availableImports)) →
      ((x : Except String ImportCompletion.AvailableImports) → motive x) → motive x