How to deal with a forIn step?

Stream: new members

[Philipp]

There was a question recently about proving the equality of two functions that sum over a list:

def recSum : List Nat → Nat
| [] => 0
| a :: as => a + recSum as

def doSum (l : List Nat) : Nat := Id.run do
  let mut acc := 0
  for a in l do
    acc := acc + a
  return acc

I thought that could be an interesting exercise so I tried writing a proof

example (l : List Nat) : recSum l = doSum l := by
  unfold doSum Id.run
  simp
  induction' l with hd tail ih
  · apply Eq.refl
  · unfold recSum
    simp[ih]
    sorry

at this point the goal state is

hd: ℕ
tail: List ℕ
ih: recSum tail = forIn tail 0 fun a r => ForInStep.yield (r + a)
⊢ (hd + forIn tail 0 fun a r => ForInStep.yield (r + a)) = forIn tail hd fun a r => ForInStep.yield (r + a)

I'm pretty lost. I guess I would want to somehow move the hd into the 0 (accumulator) on the left hand side? Like going a forIn step backwards?