exact Equiv.Set.univ (Fin (Fintype.card α))
α : Type u_1
inst : FinDenumerable α
⊢ ↑Set.univ ≃ Fin (Fintype.card α)

α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin
α : Type u_1
inst : FinDenumerable α
⊢ Function.Surjective encode_fin