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

State before:
U : Type
A : Set U
⊢ denum A ↔ Univ ℕ ∼ A
Tactic:
rfl
State after:
no goals