[ ] generalize precedence to everything, e.g. to fix printing of parentheses in 'all'.
[ ] equations for ≤, etc. (anything with transitivity)
[ ] hide the suc-oriented arithmetic
[ ] rewrite with all-quantified equations
[ ] add section on rewrite-in to the introduction
[ ] Revisit syntax for rewriting with a set of equations (replace bar)
[ ] Display overview of test results after running
[ ] create more student exercises
[ ] specify number of unfoldings in definition
[ ] remove parent param from parser, not needed anymore