∀ {α : Type u_1} (motive : (x : List α) → (x_1 : α) → x.head? = some x_1 → Prop) (x : List α) (x_1 : α)
  (x_2 : x.head? = some x_1),
  (∀ (head : α) (tail : List α) (x : α) (h : (head :: tail).head? = some x), motive (head :: tail) x h) →
    motive x x_1 x_2