∀ (motive : List ℕ → List ℕ → Sort u_1) (id₁ : ℕ) (ids₁ : List ℕ) (id₂ : ℕ) (ids₂ : List ℕ)
  (h_1 : (x : List ℕ) → motive [] x) (h_2 : (x : List ℕ) → motive x [])
  (h_3 : (id₁ : ℕ) → (ids₁ : List ℕ) → (id₂ : ℕ) → (ids₂ : List ℕ) → motive (id₁ :: ids₁) (id₂ :: ids₂)),
  (match id₁ :: ids₁, id₂ :: ids₂ with
    | [], x => h_1 x
    | x, [] => h_2 x
    | id₁ :: ids₁, id₂ :: ids₂ => h_3 id₁ ids₁ id₂ ids₂) =
    h_3 id₁ ids₁ id₂ ids₂