∀ {α : Type u_1} (motive : List (Option α) → List α → Sort u_2) (a : α) (as : List (Option α)) (as' : List α)
  (h_1 : (x : List α) → motive [] x)
  (h_2 : (a : α) → (as : List (Option α)) → (as' : List α) → motive (some a :: as) as')
  (h_3 : (as : List (Option α)) → motive (none :: as) [])
  (h_4 : (as : List (Option α)) → (a : α) → (as' : List α) → motive (none :: as) (a :: as')),
  (match some a :: as, as' with
    | [], x => h_1 x
    | some a :: as, as' => h_2 a as as'
    | none :: as, [] => h_3 as
    | none :: as, a :: as' => h_4 as a as') =
    h_2 a as as'