rw [beta_unbeta_recSequence_eq f g z v m (Nat.lt_add_right 1 hm),
  beta_unbeta_recSequence_eq f g z v (m + 1) (Nat.add_lt_add_right hm 1)]
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z
⊢ (unbeta (recSequence f g z v)).beta (m + 1) = g (m ::ᵥ (unbeta (recSequence f g z v)).beta m ::ᵥ v)
no goals