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

State before:
U : Type
A : Set U
⊢ finite A ↔ ∃ n, numElts A n
Tactic:
rfl
State after:
no goals