induction hf
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ Arith₁ f
case zero
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun x => 0

case succ
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun v => v.head.succ

case get
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Arith₁ fun v => v.get i✝

case comp
n : ℕ
f : Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
a_ih✝¹ : Arith₁ f✝
a_ih✝ : ∀ (i : Fin n✝), Arith₁ (g✝ i)
⊢ Arith₁ fun a => f✝ (ofFn fun i => g✝ i a)

case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Arith₁ f✝
a_ih✝ : Arith₁ g✝
⊢ Arith₁ fun v => rec (f✝ v.tail) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ v.tail)) v.head