simp at this
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta ↑⟨m, ⋯⟩ = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m