apply Encodable.encode_inj
case h
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ Encodable.encode w✝¹ = Encodable.encode w✝ ↔ w✝¹ = w✝
no goals