Don't fold lets if the let-bound variable occurs under a lambda-abstraction

[lukaszcz]

Currently, a let is always folded if the bound variable occurs at most once. But this is incorrect if the variable occurs under a lambda-abstraction, because the lambda may (and typically will) be passed to another function and called multiple times. This can duplicate the computation of the let-bound value, potentially even changing the asymptotic complexity.

Example:

f (lst1 lst2 : List Nat) : Bool :=
  let s := sum lst2
  in
  all (x in lst1)
    x > s;

The let-folding folds the s resulting in:

f (lst1 lst2 : List Nat) : Bool :=
  all (x in lst1)
    x > sum lst2;

The computation of sum lst2 was moved inside the loop.