(motive : List Lean.Name → Sort u_1) →
  (x : List Lean.Name) →
    (Unit → motive []) →
      ((is : List Lean.Name) →
          (i : Lean.Name) → (tail : List Lean.Name) → (h : is = i :: tail) → motive (namedPattern is (i :: tail) h)) →
        motive x