suffices ∀ L i (hL : L = toList (univ α)), List.get L i = fromFin (i.cast (by simp [hL]))
  from this _ _ rfl
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ (toList (univ α)).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 α)), L.get i = fromFin (Fin.cast ⋯ i)