fun_trans can't see through let bindings

[lecopivo]

When running simp/fun_trans with zeta:=false, the tactic fun_prop is unable to see through let bindings. For example this does is not provable:

import SciLean

open SciLean

variable
  {K : Type} [RealScalar K]
  {X : Type} [Vec K X]
  {ι : Type} {κ : Type} [IndexType ι] [IndexType κ]

set_default_scalar K

example (f : X → X) (hf : CDifferentiable K f)
  : (∂ x, let df := ∂ (x':=0), f x'
          df x + df x)
    =
    let df := ∂ (x':=0), f x';
    fun x dx => ∂ (x:=x;dx), df x + ∂ (x:=x;dx), df x :=
by
  conv =>
    lhs; autodiff
  sorry

This is because simp introduces new (non-let) free variable df when differentiating df x + df x. This prevents fun_prop unfolding df.