∀ {α : Type u_2} (n : ℕ) (motive : { i // i ≤ n } → α → Sort u_1) (i : ℕ) (h : i + 1 ≤ n) (x : α)
  (h_1 : (property : 0 ≤ n) → (x : α) → motive ⟨0, property⟩ x)
  (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → (x : α) → motive ⟨i.succ, h⟩ x),
  (match ⟨i.succ, h⟩, x with
    | ⟨0, property⟩, x => h_1 property x
    | ⟨i.succ, h⟩, x => h_2 i h x) =
    h_2 i h x