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

State before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : ι → α
⊢ fintypeArrowEquivFinArrow f = fun i => f (fintypeEquivFin.symm i)
Tactic:
rfl
State after:
no goals