saw-core pretty printer should preserve more sharing

[brianhuffman]

When saw-core terms are printed with print_term or print_goal, shared subterms are printed once in a single top-level let block. However, shared subterms that refer to lambda-bound variables cannot be moved outside the lambda, and so those get printed in expanded form. This situation is very common for proof goals, where the goal term starts with lambdas for all the quantified variables. This makes print_goal much less useful.

In addition to a top-level let block for shared closed subterms, the term pretty printer should also produce let blocks under lambdas for shared subterms that mention that bound variable.