∀ (motive : Lean.Name → Sort u_1) (x : Lean.Name) (h_1 : (pre : Lean.Name) → (str : String) → motive (pre.str str))
  (h_2 : (x : Lean.Name) → motive x),
  (∀ (pre : Lean.Name) (str : String), x = pre.str str → False) →
    (match x with
      | pre.str str => h_1 pre str
      | x => h_2 x) =
      h_2 x