∀ {α : Type u_1} (motive : List α → Sort u_2) (α_1 : Sort u✝) (β : α_1 → Sort v✝) (f : (x : α_1) → β x)
  (rel : List α → α_1 → Prop) (x : List α) (h_1 : Unit → ((y : α_1) → rel [] y → β y) → motive [])
  (h_2 : (x : α) → ((y : α_1) → rel [x] y → β y) → motive [x])
  (h_3 : (x y : α) → (l : List α) → ((y_1 : α_1) → rel (x :: y :: l) y_1 → β y_1) → motive (x :: y :: l)),
  ((match (motive := (x : List α) → ((y : α_1) → rel x y → β y) → motive x) x with
      | [] => fun x => h_1 a x
      | [x] => fun x_1 => h_2 x x_1
      | x :: y :: l => fun x_1 => h_3 x y l x_1)
      fun y h => f y) =
    match x with
    | [] => h_1 a fun y h => f y
    | [x] => h_2 x fun y h => f y
    | x :: y :: l => h_3 x y l fun y_1 h => f y_1