(motive : Lean.Name → Lean.Name → Sort u_1) →
  (n suff : Lean.Name) →
    ((p : Lean.Name) → (s : String) → (suff : Lean.Name) → motive (p.str s) suff) →
      ((x suff : Lean.Name) → motive x suff) → motive n suff