`lsimp` is not fully normalizing let bindings through application

[lecopivo]

lsimp is not fully normalizing let bindings through application. Consider this code

import SciLean
#check 
  (a + 
    (a + 
    let x := a + a
    x))
  rewrite_by
    lsimp (config := {zeta := false, singlePass := true})

which produces

a +
  let x := a + a;
  a + x : ℕ

but

let x := a + a;
a + (a + x)

is expected