intro acc
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α),
    (if h : n < n then ofFn.go f (n + 1) (push acc (f { val := n, isLt := h })) else acc) =
      acc ++ if h : n < n then ofFn.go f (n + 1) (push #[] (f { val := n, isLt := h })) else #[]
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ (if h : n < n then ofFn.go f (n + 1) (push acc (f { val := n, isLt := h })) else acc) =
    acc ++ if h : n < n then ofFn.go f (n + 1) (push #[] (f { val := n, isLt := h })) else #[]