rw [h_ind (acc.push _), h_ind (#[].push _)]
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ ofFn.go f (i + 1) (push acc (f { val := i, isLt := hi })) =
    acc ++ ofFn.go f (i + 1) (push #[] (f { val := i, isLt := hi }))
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ push acc (f { val := i, isLt := hi }) ++ ofFn.go f (Nat.succ i) #[] =
    acc ++ (push #[] (f { val := i, isLt := hi }) ++ ofFn.go f (Nat.succ i) #[])