constructor
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j ↔ i = j
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j → i = j

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ i = j → toFin i = toFin j