rintro rfl
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ x = y → toFin x = toFin y
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x : ι
⊢ toFin x = toFin x