dsimp
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) (Nat.succ k) →
        (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) k
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = acc ++ ofFn.go f (Nat.succ k) #[]) →
        ∀ (acc : Array α), ofFn.go f k acc = acc ++ ofFn.go f k #[]