by_cases i < n
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
case pos
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
h✝ : i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]

case neg
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
h✝ : ¬i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]