∀ {α : Type u_1} (motive : (x : List α) → 0 < x.length → Prop) (x : List α) (x_1 : 0 < x.length),
  (∀ (head : α) (tail : List α) (x : 0 < (head :: tail).length), motive (head :: tail) x) → motive x x_1