∀ {c : Nat.Partrec.Code} {n x : ℕ} (motive : (∃ k, x ∈ Nat.Partrec.Code.evaln k c n) → Prop)
  (x_1 : ∃ k, x ∈ Nat.Partrec.Code.evaln k c n),
  (∀ (k : ℕ) (h : x ∈ Nat.Partrec.Code.evaln k c n), motive ⋯) → motive x_1