{motive : Lean.Lsp.LeanStaleDependencyParams → Sort u} →
  ((staleDependency : Lean.Lsp.DocumentUri) → motive { staleDependency := staleDependency }) →
    (t : Lean.Lsp.LeanStaleDependencyParams) → motive t