rw [LawfulIndexType.toList_eq_ofFn] at hL
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.get i = fromFin (Fin.cast ⋯ i)
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL✝ : L = toList (univ α)
hL : L = List.ofFn fromFin
⊢ L.get i = fromFin (Fin.cast ⋯ i)