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

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
i : ι
v : Vector α (Fintype.card ι)
⊢ fintypeArrowEquivVector.symm v i = v.get (fintypeEquivFin i)
Tactic:
rfl
State after:
no goals