apply Eq.symm
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ some (Option.get (Encodable.decode ↑n) ⋯) = Encodable.decode₂ α ↑n
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode₂ α ↑n = some (Option.get (Encodable.decode ↑n) ⋯)