[ ] generalize precedence to everything, e.g. to fix printing of parentheses in 'all'.
[ ] don't import lemmas
[ ] equations for ≤, etc. (anything with transitivity)
[ ] hide the suc-oriented arithmetic
[ ] rewrite with all-quantified equations
[ ] add section on rewrite-in to the introduction
[ ] implicit instantiation for all's [x] in an apply [ ] in checking mode, as part of check_implies?
[ ] print char_fun(λx{false}) as ∅
[ ] issue of conjunction intro in checking mode
[ ] Revisit syntax for rewriting with a set of equations (replace bar)
[ ] Fix syntax error messages inside imports
[ ] create a test feature that adds support for [ ] random number generation [ ] error (halt with message) [ ] loops?
[ ] create student exercises
[ ] specify number of unfoldings in definition
[ ] remove parent param from parser, not needed anymore