constructor
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j ↔ i = j
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j → i = j

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ i = j → fromFin i = fromFin j