simp[encode_finArrow, encode_list (List.ofFn f)]
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode f = encode fun i => encode (f i)
β : Type u_1
inst✝¹ : Encodable β
k : ℕ
inst✝ : Primcodable β
f : Fin k → β
⊢ encode ∘ f = fun i => encode (f i)