∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (is : List α) (h_1 : (is : List α) → motive [] is)
  (h_2 : (t : α) → (ts is : List α) → motive (t :: ts) is),
  (match [], is with
    | [], is => h_1 is
    | t :: ts, is => h_2 t ts is) =
    h_1 is