ext i x
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).data = List.map f (List.fins n)
case a.a
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ x ∈ List.get? (ofFn f).data i ↔ x ∈ List.get? (List.map f (List.fins n)) i