∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (a' : α) → (b : β a') → (l : List (Sigma β)) → motive (⟨a', b⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨a', b⟩ :: l => h_2 a' b l) =
    h_1 ()