rw[Encodable.encode_ofEquiv, encode_vector]
β : Type u_1
inst✝ : Encodable β
n : ℕ
f : Fin n → β
⊢ encode f = encode (List.ofFn f)
β : Type u_1
inst✝ : Encodable β
n : ℕ
f : Fin n → β
⊢ encode ((Equiv.vectorEquivFin β n).symm f).toList = encode (List.ofFn f)