{motive : Lean.Lsp.LeanModule → Sort u} →
  (t : Lean.Lsp.LeanModule) →
    ((name : String) →
        (uri : Lean.Lsp.DocumentUri) →
          (data? : Option Lean.Json) → motive { name := name, uri := uri, data? := data? }) →
      motive t