Enable let expressions with weakly pure subexpressions

[jcp19]

This PR allows us to write assertions such as the following:

let z := y in Q(z)
let z := x in acc(z)

So far, these assertions were rejected because Q(z) and acc(z) are not strongly pure.

Furthermore, I moved the desugaring of strongly pure let expressions from exprD to ghostExprD

[jcp19]

PS: the tests are passing, but the CI is reporting failures due to non-deterministic factors