∀ {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : (i : ℕ) → α → i < (xs ++ ys).size → β},
  (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun i a h => f i a ⋯) ++ ys.mapFinIdx fun i a h => f (i + xs.size) a ⋯