Theorem: IndexType.card_unit (SciLean/Data/IndexType.lean)

State before:
ι : Type v
inst✝ : IndexType ι
⊢ card Unit = 1
Tactic:
rfl
State after:
no goals