no goals
f : Code → ℕ →. ℕ
hf : Partrec₂ f
cf : Code
ef : eval cf = fun n => Part.bind ↑(decode n) fun a => Part.map encode ((fun p => f p.fst p.snd) a)
c : Code
e : eval (curry cf (encode c)) = eval c
n : ℕ
⊢ eval c n = f c n
simp [e.symm, ef, Part.map_id']