rw [LawfulIndexType.toList_eq_ofFn]
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (toList (univ α)).length = card α
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (List.ofFn fromFin).length = card α