cases h
α : 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) })
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ ofFn.go f n acc =
    push (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) n acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })