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