It's not obvious why the simplifier generates code that correctly satisfies
the let/app invariant.   This patch does some minor refactoring, but the main
point is to document pre-conditions to key functions, namely that the rhs
passed in satisfies the let/app invariant.

There shouldn't be any change in behaviour.