keep less unused symbols

For the purpose of counterexamples, a lot of variables introduced with let that are kept as let definition, even if they are substituted in the body of the let.

This feature is needed only for some variables, e.g. the ones that store the results of function calls. It should be possible to identify these variables when they are generated in vc.ml, say with a specific attribute keep_even_unused. If this was done, then the keeping of such "unused" variables could be relaxed and done only when the attribute in question is present.