Improve handling of precondition checking

[joscoh]

Currently, the precondition checking in expressions follows the following rules:

1. given p => e, all precondition-assertions in e can assume p
2. given if p then e1 else e2, all precondition assertions in e1 can assume p and all in e2 can assume not p

We would like to add:
3. given p || e, all precondition assertions in e can assume not p
4. given p /\ e, all precondition assertions in e can assume p

And likely (using a lambda-based encoding for let):
5. given let x := e1 in e, preconditions in e1 are added only at the point where x is used in e (which can be in a context including some of the assumptions from the previous rules)