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