∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop},
  motive (fun x => 0) Nat.Primrec'.zero →
    motive (fun v => v.head.succ) Nat.Primrec'.succ →
      (∀ {n : ℕ} (i : Fin n), motive (fun v => v.get i) ⋯) →
        (∀ {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ) (a : Nat.Primrec' f)
            (a_1 : ∀ (i : Fin n), Nat.Primrec' (g i)),
            motive f a → (∀ (i : Fin n), motive (g i) ⋯) → motive (fun a => f (List.Vector.ofFn fun i => g i a)) ⋯) →
          (∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} (a : Nat.Primrec' f)
              (a_1 : Nat.Primrec' g),
              motive f a →
                motive g a_1 → motive (fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) ⋯) →
            ∀ {n : ℕ} {a : List.Vector ℕ n → ℕ} (t : Nat.Primrec' a), motive a t