{motive : Turing.ToPartrec.Code → Sort u} →
  (t : Turing.ToPartrec.Code) →
    motive Turing.ToPartrec.Code.zero' →
      motive Turing.ToPartrec.Code.succ →
        motive Turing.ToPartrec.Code.tail →
          ((a a_1 : Turing.ToPartrec.Code) → motive a → motive a_1 → motive (a.cons a_1)) →
            ((a a_1 : Turing.ToPartrec.Code) → motive a → motive a_1 → motive (a.comp a_1)) →
              ((a a_1 : Turing.ToPartrec.Code) → motive a → motive a_1 → motive (a.case a_1)) →
                ((a : Turing.ToPartrec.Code) → motive a → motive a.fix) → motive t