∀ (motive : Nat.Partrec.Code → Sort u_1) (cf cg : Nat.Partrec.Code) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match cf.prec cg with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_7 cf cg