Theorem: Encodable.encode_finArrow (Logic/Vorspiel/Computability.lean)

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

State before:
β : Type u_1
inst✝ : Encodable β
n : ℕ
f : Fin n → β
⊢ encode ((Equiv.vectorEquivFin β n).symm f).toList = encode (List.ofFn f)
Tactic:
simp
State after:
no goals