Improve calculus of (quantified) variables dependencies of let bindings

[iguerNL]

Currently, given an example:

logic f : int -> int
logic g : int, int -> int
logic P : int, int, int -> prop

axiom a:
  forall x, y : int.
    let v = f(x) in
    let w = g(v, v) + f(x) in
    P(v, w, y) and P(w, y, v)

goal g: false

Axiom a is transformed internally to:

forall 'x~2':int, 'y~3':int[<triggers>].
 (let [sko = !?___let2('y~3','x~2')] 'v~4' = f('x~2') in
(let [sko = !?___let1('v~4','y~3','x~2')] 'w~5' =
(g('v~4','v~4') + f('x~2')) in
(P('w~5','y~3','v~4') /\ P('v~4','w~5','y~3')))))"

The important thing that should be noticed in the transformation is that v~4 is associated to a fresh symbol (application) !?___let2('y~3','x~2') and 'w~5' is associated to a fresh symbol !?___let1('v~4','y~3','x~2')

I would say that:

• v~4 has actually no dependency to 'y~3' (because it's equal to f('x~2'), which does not contain 'y~3'), so !?___let2('y~3','x~2') could be simplified
• by transitivity, we could say that 'w~5' only has a dependency to 'x~2'. So, its fresh symbol would become: !?___let1('x~2')

In particular, for quantifier-free formulas, the introduced fresh symbols are just constants (which is not the case currently).

@Gbury @Coquera What do you think about the analysis ? Do you see any eventual soundness bug in this simplification ?