simp[Vector.get_one]
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))
⊢ ∀ (i : Vector ℕ (n + 2)),
    ((i.get 1).ball fun i_1 => (i.head.beta (i_1 + 1)).isEqNat (g (i_1 ::ᵥ i.head.beta i_1 ::ᵥ i.tail.tail))) =
      i.tail.head.ball fun i_1 => (i.head.beta (i_1 + 1)).isEqNat (g (i_1 ::ᵥ i.head.beta i_1 ::ᵥ i.tail.tail))
no goals