Theorem: Primrec.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 γ
k : ℕ
α : Type u_5
inst✝ : Primcodable α
this : Primrec fun e => encode (decode e)
e : ℕ
⊢ encode (decode e) = encode (Option.map List.ofFn (decode e))
Tactic:
rcases (Encodable.decode e) <;> simp[Encodable.encode_finArrow]
State after:
no goals