lsimp projection sees through let bindings

[lecopivo]

In some cases projections can destroy let bindings in lsimp

#check 
   (fun i : Nat =>
      let j := 42
      let foo := ((i * j, i+j), (i ^ j, i / j))
      foo.fst.snd)
   rewrite_by
     lsimp (config := {zeta:=false}) only

returns

(fun i : Nat =>
      let j := 42
      i + j)

which is undesirable. We want to split foo intor four let bindings

   (fun i : Nat =>
      let j := 42
      let foo := ((i * j, i+j), (i ^ j, i / j))
      foo.fst.snd)
==>
   (fun i : Nat =>
      let j := 42
      let foo_fst_fst := (i * j)
      let foo_fst_snd:= (i+j)
      let foo_snd_fst := (i ^ j)
      let foo_snd_snd := (i / j)
      ((foo_fst_fst, foo_fst_snd),(foo_snd_fst,foo_snd_snd)).fst.snd)
==>
   (fun i : Nat =>
      let j := 42
      let foo_fst_snd:= (i+j)
      foo_fst_snd)

Such transformation is currently part of let_normalize but should be an integral part of lsimp

[lecopivo]

This is problem again but with how Tactic.lift_lets_simproc works now.