case pos hlt =>
  refine Nat.recAscend (motive:=λ i => ∀ acc, Array.ofFn.go f i acc = acc ++ Array.ofFn.go f i #[]) (n:=n) ?_ ?_ i (Nat.le_of_lt hlt) acc
  . dsimp; unfold Array.ofFn.go
    intro acc
    rw [dif_neg (Nat.lt_irrefl n), dif_neg (Nat.lt_irrefl n)]
    rfl
  . dsimp
    intro i hi h_ind acc
    unfold Array.ofFn.go
    rw [dif_pos hi, dif_pos hi]
    rw [h_ind (acc.push _), h_ind (#[].push _)]
    conv =>
      rhs; rw [←Array.append_assoc]
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
no goals