∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k))
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k))
  (h_5 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)),
  (match Turing.ToPartrec.Cont.comp f k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ fs as k => h_2 fs as k
    | Turing.ToPartrec.Cont.cons₂ ns k => h_3 ns k
    | Turing.ToPartrec.Cont.comp f k => h_4 f k
    | Turing.ToPartrec.Cont.fix f k => h_5 f k) =
    h_4 f k