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⟩
case intro.intro.intro
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∃ a,
    (true = (decide (a.beta 0 = f v.tail) && decide (∀ m < v.head, a.beta (m + 1) = g (m ::ᵥ a.beta m ::ᵥ v.tail))) ∧
        ∀ {m : ℕ},
          m < a →
            false =
              (decide (m.beta 0 = f v.tail) &&
                decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))) ∧
      a.beta v.head = rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
no goals