∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 :
    (l₁ : List α) →
      (hd₁ : α) → (tl₁ : List α) → l₁ = hd₁ :: tl₁ → (hd₂ : α) → (tl₂ : List α) → motive (hd₁ :: tl₁) (hd₂ :: tl₂)),
  (match [], x with
    | [], x => h_1 x
    | x, [] => h_2 x
    | l₁@h:(hd₁ :: tl₁), hd₂ :: tl₂ => h_3 l₁ hd₁ tl₁ h hd₂ tl₂) =
    h_1 x