- adress normalizing of terms with context push (and other typos)
- Remark on missing Gamma

- replace semantic by semantics
- apply some review suggestions

this looks less ragged

The simplification `(P -> Q) -> Q => P or Q` is already covered
by `bool_simplify`.

- include Changelog
- Adapt index tables
- Add rule description environments
- finish adaption of the proof rule description

- Add backport goal to Makefile to aid work
- copy the main chapter as "spec.tex"
- copy the rules appendix as "alethe_rules.tex"
- finish adaption of source code in spec.tex

- Define what a valid Alethe proof is formally
- Show that a valid Alethe proof is sound
- TODO: nicer handling of let