Changes

Summary

1. more uniform use of Reconstruct.clean_proof_of;
2. clarified message: print subgoal number instead of potentially large term;
3. tuned;
4. suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';
5. tuned;