Changes

Summary

1. examples and documentation for code generator time measurements
2. optional timing for code generator conversions
3. clarified internal interfaces
4. tuned
5. delegate inclusion of required dictionaries to user-space instead of half-working magic
6. corrected closure scope of static_conv_thingol; clarified implementation and names
7. clarified proof context vs. background theory
8. explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
9. clarified naming conventions and code for code evaluation sandwiches
10. clarified names of variants