induction x using cons_induction generalizing i with
| empty => cases hi
| cons a x IH =>
  simp only [mapIdx_cons]
  cases i with
  | zero => simp only [Nat.zero_eq, get_cons_zero]
  | succ i =>
    simp only [Nat.zero_eq, Nat.succ_eq_add_one]
    rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
    rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
    exact IH ..
α : Type u
β : Type v
γ : Type w
n : Nat
f : Fin n → α → β
x : SizedArray α n
i : Nat
hi : i < n
⊢ (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
no goals