simp only [Nat.zero_eq, Nat.succ_eq_add_one]
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[Nat.succ i] =
    f { val := Nat.succ i, isLt := hi } (cons a x)[Nat.succ i]
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i + 1] =
    f { val := i + 1, isLt := hi } (cons a x)[i + 1]