∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop} {a : ℕ → ℕ} (t : Nat.Primrec a),
  motive (fun x => 0) Nat.Primrec.zero →
    motive Nat.succ Nat.Primrec.succ →
      motive (fun n => (Nat.unpair n).1) Nat.Primrec.left →
        motive (fun n => (Nat.unpair n).2) Nat.Primrec.right →
          (∀ {f g : ℕ → ℕ} (a : Nat.Primrec f) (a_1 : Nat.Primrec g),
              motive f a → motive g a_1 → motive (fun n => Nat.pair (f n) (g n)) ⋯) →
            (∀ {f g : ℕ → ℕ} (a : Nat.Primrec f) (a_1 : Nat.Primrec g),
                motive f a → motive g a_1 → motive (fun n => f (g n)) ⋯) →
              (∀ {f g : ℕ → ℕ} (a : Nat.Primrec f) (a_1 : Nat.Primrec g),
                  motive f a →
                    motive g a_1 →
                      motive (Nat.unpaired fun z n => Nat.rec (f z) (fun y IH => g (Nat.pair z (Nat.pair y IH))) n) ⋯) →
                motive a t