{motive : Lean.Lsp.TextDocumentSyncOptions → Sort u} →
  ((openClose : Bool) →
      (change : Lean.Lsp.TextDocumentSyncKind) →
        (willSave willSaveWaitUntil : Bool) →
          (save? : Option Lean.Lsp.SaveOptions) →
            motive
              { openClose := openClose, change := change, willSave := willSave, willSaveWaitUntil := willSaveWaitUntil,
                save? := save? }) →
    (t : Lean.Lsp.TextDocumentSyncOptions) → motive t