intro _ h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∀ (a : α), a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n → Encodable.decode ↑n = some a
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a✝ : α
h : a✝ ∈ Encodable.decode ↑n ∧ Encodable.encode a✝ = ↑n
⊢ Encodable.decode ↑n = some a✝