rw [Encodable.decode₂_is_partial_inv]
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode₂ α ↑n = some (Option.get (Encodable.decode ↑n) ⋯)
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n