unfold ofFn.go
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ ofFn.go f i acc =
    push (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) i acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ (if h : i < n + 1 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    push
      (if h : i < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (i + 1)
          (push acc (f { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })