- fix bitrot of pretty printer
- add support for metavariables in types
- split off definitions of reductions to separate file
- example use of metavars in quantifiers cut-elim
- some introductory text