{motive : Lean.Lsp.CreateFile.Options → Sort u} →
  (t : Lean.Lsp.CreateFile.Options) →
    ((overwrite ignoreIfExists : Bool) → motive { overwrite := overwrite, ignoreIfExists := ignoreIfExists }) → motive t