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