∀ {α : Type u_1} (motive : ℕ → Array α → Sort u_2) (xs : Array α) (h_1 : (xs : Array α) → motive 0 xs)
  (h_2 : (n : ℕ) → (xs : Array α) → motive n.succ xs),
  (match 0, xs with
    | 0, xs => h_1 xs
    | n.succ, xs => h_2 n xs) =
    h_1 xs