{motive : Lean.Lsp.DeleteFile → Sort u} →
  (t : Lean.Lsp.DeleteFile) →
    ((uri : Lean.Lsp.DocumentUri) →
        (options? : Option Lean.Lsp.DeleteFile.Options) →
          (annotationId? : Option String) →
            motive { uri := uri, options? := options?, annotationId? := annotationId? }) →
      motive t