Recursively traverse let expressions when inferring triggers, not just once

[marcoeilers]

Fixes Silicon issue viperproject/silicon#943.

[Aurel300]

Should we contribute a minimised test case? Is the verification for this acceptable?

[marcoeilers]

The verification time for the test case is under two seconds in both backends.
But yes, if you can come up with a minimised test case for this, I'd be very happy to add that. It's not super trivial though; I can easily write an example where Viper can now find a trigger but couldn't before, but it's not as easy to write an example where Z3 then doesn't just infer the trigger itself.