simp[encode_fintypeArrow, encode_finArrow, hι]
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
hι : Fintype.card ι = 2
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = encode [f (fintypeEquivFin.symm (Fin.cast ⋯ 0)), f (fintypeEquivFin.symm (Fin.cast ⋯ 1))]
no goals