{motive : Lean.Lsp.InsertReplaceEdit → Sort u} →
  ((newText : String) →
      (insert replace : Lean.Lsp.Range) → motive { newText := newText, insert := insert, replace := replace }) →
    (t : Lean.Lsp.InsertReplaceEdit) → motive t