intro n
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (n : Fin (Fintype.card α)), Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n