`ftrans` unfold let bindings sometimes

[lecopivo]

ftrans seems to unfold let bindings sometimes. Especially if the value of let binding is lambda function

-- 0 : ℕ
#check 
  (let f := fun i : Nat => i ; (f 0))
  rewrite_by
    ftrans only

or

variable (f : X → Nat → Y) (x : X)

-- ∂ (x':=x), f x' 0 : X → Y
#check 
  (let ydf := fun i => ∂ x':=x, f x' i; (ydf 0))
  rewrite_by
    ftrans only

expected output is

let f := fun i => i;
  f 0

and

let ydf := fun i => ∂ (x':=x), f x' i;
  ydf 0let ydf := fun i => ∂ (x':=x), f x' i;
  ydf 0