have hp : @Arith₁ (n + 3) (fun v =>
  isEqNat (Nat.beta v.tail.head (v.head + 1))
  (g (v.head ::ᵥ Nat.beta v.tail.head v.head ::ᵥ v.tail.tail.tail))) :=
  (equal 0 1).comp₂ _
    ((beta 0 1).comp₂ _ head.tail ((succ 0).comp₁ _ head))
    (hg.comp' $ head.cons $ ((beta 0 1).comp₂ _ head.tail head).cons $ by intro i; simp; exact proj _)
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)))
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
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))
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head