simp [<- pa]
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ Encodable.decode ↑n = some a
no goals