exact (ArithPart₁.map (fun v x => Nat.beta x v.head) this (ArithPart₁.rfindPos hF)).of_eq <| by
  intro v
  simp only [add_succ_sub_one, head_cons, tail_cons, and_pos_iff, isEqNat_pos_iff,
    ball_pos_iff, Bool.decide_and, PFun.coe_val, eq_some_iff, mem_map_iff, mem_rfind,
    mem_some_iff, F]
  suffices ∃ z : ℕ, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail) by
    rcases least_number _ this with ⟨z, ⟨hz0, hzs⟩, hzm⟩
    exact ⟨z, ⟨by symm; simp[hz0]; exact hzs,
      by intro m hm; symm; simpa[imp_iff_not_or, not_or] using hzm m hm⟩,
      beta_eq_rec f g hz0 hzs⟩
  let l : List ℕ := recSequence f g v.head v.tail
  exact ⟨unbeta l,
    beta_unbeta_recSequence_zero f g v.head v.tail,
    fun i hi => beta_unbeta_recSequence_succ f g v.head v.tail hi⟩
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
hF : Arith₁ F
this : Arith₁ fun v => v.head.beta v.tail.head
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
no goals