∀ (x : List ℕ) (fs : Turing.ToPartrec.Code) (as : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.cons₁ fs as k) x =
    Turing.ToPartrec.stepNormal fs (Turing.ToPartrec.Cont.cons₂ x k) as