∀ {α : Type u_1} (motive : (x : List α) → Fin x.length → Sort u_2) (a : α) (tail : List α)
  (isLt : 0 < (a :: tail).length)
  (h_1 : (a : α) → (tail : List α) → (isLt : 0 < (a :: tail).length) → motive (a :: tail) ⟨0, isLt⟩)
  (h_2 : (head : α) → (as : List α) → (i : ℕ) → (h : i.succ < (head :: as).length) → motive (head :: as) ⟨i.succ, h⟩),
  (match a :: tail, ⟨0, isLt⟩ with
    | a :: tail, ⟨0, isLt⟩ => h_1 a tail isLt
    | head :: as, ⟨i.succ, h⟩ => h_2 head as i h) =
    h_1 a tail isLt