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

State before:
ι✝ : Type v
inst✝² : IndexType ι✝
ι : Type u_1
κ : Type u_2
inst✝¹ : IndexType ι
inst✝ : IndexType κ
⊢ card (ι ⊕ κ) = card ι + card κ
Tactic:
rfl
State after:
no goals