case neg hnlt =>
  unfold Array.ofFn.go
  rw [dif_neg hnlt, dif_neg hnlt]
  rfl
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
no goals