(motive : Lean.Syntax.Range × String × String → Sort u_1) →
  (x : Lean.Syntax.Range × String × String) →
    ((rg : Lean.Syntax.Range) → (before after : String) → motive (rg, before, after)) → motive x