apply (decode_partial_inv n).imp
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a, Encodable.decode ↑n = some a
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∀ (a : α), a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n → Encodable.decode ↑n = some a