unfold ofFn.go
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ ofFn.go f i acc = acc
α : Type u
f : Fin 0 → α
i : Nat
acc : Array α
⊢ (if h : i < 0 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) = acc