induction hf
n : ℕ
f : Vector ℕ n →. ℕ
hf : ArithPart₁ f
⊢ Partrec' f
case zero
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0

case one
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1

case add
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝ + v.get j✝

case mul
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝ * v.get j✝

case proj
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝

case equal
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => (v.get i✝).isEqNat (v.get j✝)

case lt
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => (v.get i✝).isLtNat (v.get j✝)

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

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