simp
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type ?u.1841
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ (toList (univ α)).length = card α
no goals