∀ {f : Nat.Partrec.Code → ℕ →. ℕ}
  (motive :
    (∃ c, c.eval = fun n => (↑(Encodable.decode n)).bind fun a => Part.map Encodable.encode ((fun p => f p.1 p.2) a)) →
      Prop)
  (x : ∃ c, c.eval = fun n => (↑(Encodable.decode n)).bind fun a => Part.map Encodable.encode ((fun p => f p.1 p.2) a)),
  (∀ (cf : Nat.Partrec.Code)
      (ef :
        cf.eval = fun n => (↑(Encodable.decode n)).bind fun a => Part.map Encodable.encode ((fun p => f p.1 p.2) a)),
      motive ⋯) →
    motive x