How to prove that a recursively defined function is equal to

Stream: new members

[Asei Inoue]

import Mathlib.Tactic

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

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

example : recSum [0,1,4] = 5 := by rfl

example : doSum [0,1,4,2,10] = 17 := by rfl

example (l : List Nat) : recSum l = doSum l := by
  -- I want to show this
  sorry

Thank you.