simp [LawfulIndexType.toList_eq_ofFn, List.mem_ofFn]
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ x ∈ toList (univ α)
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ ∃ y, fromFin y = x