simp[encode_fintypeArrow, encode_finArrow, this]
β✝ : Type u_1
inst✝⁵ : Encodable β✝
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : Primcodable ι
inst✝² : DecidableEq ι
inst✝¹ : IsEmpty ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
this : Fintype.card ι = 0
⊢ encode f = 0
no goals