Theorem: FinDenumerable.encode_fin_eq_encode (FormalSystems/Preliminaries/FinDenumerable.lean)

State before:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (a : α), ↑(encode_fin a) = Encodable.encode a
Tactic:
simp [encode_fin]
State after:
no goals