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