induction hf
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
⊢ ArithPart₁ f
case prim
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
a✝ : Primrec' f✝
⊢ ArithPart₁ ↑f✝

case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f✝
a✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
a_ih✝¹ : ArithPart₁ f✝
a_ih✝ : ∀ (i : Fin n✝), ArithPart₁ (g✝ i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g✝ i v) >>= f✝

case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
a_ih✝ : ArithPart₁ ↑f✝
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))