Theorem: Primrec.sigma_finArrow_list_ofFn (Logic/Vorspiel/Computability.lean)

State before:
σ : Type u_1
α✝ : Type u_2
β : α✝ → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α✝
inst✝⁵ : (a : α✝) → Fintype (β a)
inst✝⁴ : (a : α✝) → DecidableEq (β a)
inst✝³ : (a : α✝) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
α : Type u_5
inst✝ : Primcodable α
this : Primrec fun p => (encode p).unpair.2
x✝ : (k : ℕ) × (Fin k → α)
k : ℕ
v : Fin k → α
⊢ (encode ⟨k, v⟩).unpair.2 = encode (List.ofFn ⟨k, v⟩.snd)
Tactic:
simp[encode_finArrow]
State after:
no goals