∀ {motive : (a : ℕ →. ℕ) → Nat.Partrec a → Prop}
  {motive_1 : {a : ℕ →. ℕ} → (t : Nat.Partrec a) → Nat.Partrec.below t → Prop},
  motive_1 Nat.Partrec.zero ⋯ →
    motive_1 Nat.Partrec.succ ⋯ →
      motive_1 Nat.Partrec.left ⋯ →
        motive_1 Nat.Partrec.right ⋯ →
          (∀ {f g : ℕ →. ℕ} (a : Nat.Partrec f) (a_1 : Nat.Partrec g) (ih : Nat.Partrec.below a) (a_ih : motive f a)
              (ih_1 : Nat.Partrec.below a_1) (a_ih_1 : motive g a_1),
              motive_1 a ih → motive_1 a_1 ih_1 → motive_1 ⋯ ⋯) →
            (∀ {f g : ℕ →. ℕ} (a : Nat.Partrec f) (a_1 : Nat.Partrec g) (ih : Nat.Partrec.below a) (a_ih : motive f a)
                (ih_1 : Nat.Partrec.below a_1) (a_ih_1 : motive g a_1),
                motive_1 a ih → motive_1 a_1 ih_1 → motive_1 ⋯ ⋯) →
              (∀ {f g : ℕ →. ℕ} (a : Nat.Partrec f) (a_1 : Nat.Partrec g) (ih : Nat.Partrec.below a) (a_ih : motive f a)
                  (ih_1 : Nat.Partrec.below a_1) (a_ih_1 : motive g a_1),
                  motive_1 a ih → motive_1 a_1 ih_1 → motive_1 ⋯ ⋯) →
                (∀ {f : ℕ →. ℕ} (a : Nat.Partrec f) (ih : Nat.Partrec.below a) (a_ih : motive f a),
                    motive_1 a ih → motive_1 ⋯ ⋯) →
                  ∀ {a : ℕ →. ℕ} {t : Nat.Partrec a} (t_1 : Nat.Partrec.below t), motive_1 t t_1