rewrite [length_ofFn]
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < length (ofFn f)
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < n