Theorem: HTPI.numElts_def (HTPILib/Chap8Part1.lean)

State before:
U : Type
A : Set U
n : ℕ
⊢ numElts A n ↔ I n ∼ A
Tactic:
rfl
State after:
no goals