∀ (motive : List ℕ → List ℕ → Sort u_1) (α : Sort u✝) (β : α → Sort v✝) (f : (x : α) → β x)
  (rel : List ℕ → List ℕ → α → Prop) (x x_1 : List ℕ) (h_1 : (x : List ℕ) → ((y : α) → rel [] x y → β y) → motive [] x)
  (h_2 : (x : List ℕ) → ((y : α) → rel x [] y → β y) → motive x [])
  (h_3 :
    (id₁ : ℕ) →
      (ids₁ : List ℕ) →
        (id₂ : ℕ) →
          (ids₂ : List ℕ) → ((y : α) → rel (id₁ :: ids₁) (id₂ :: ids₂) y → β y) → motive (id₁ :: ids₁) (id₂ :: ids₂)),
  ((match (motive := (x x_2 : List ℕ) → ((y : α) → rel x x_2 y → β y) → motive x x_2) x, x_1 with
      | [], x => fun x_2 => h_1 x x_2
      | x, [] => fun x_2 => h_2 x x_2
      | id₁ :: ids₁, id₂ :: ids₂ => fun x => h_3 id₁ ids₁ id₂ ids₂ x)
      fun y h => f y) =
    match x, x_1 with
    | [], x => h_1 x fun y h => f y
    | x, [] => h_2 x fun y h => f y
    | id₁ :: ids₁, id₂ :: ids₂ => h_3 id₁ ids₁ id₂ ids₂ fun y h => f y