this looks less ragged

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

- Adapt index tables
- Add rule description environments
- Adapt first rule

- Add infrastructure for Alethe proofs
- Add infrastructure for minted
- Many replacements

- {\smt} -> SMT
- Add bibliography
- Change \in{Foo}[bar] to Foo~\ref{bar}
- \about[..] -> \ref

This served as the introduction to the entire chapter in the
thesis.

- Add backport goal to Makefile to aid work
- copy the main chapter as "spec.tex"
- copy the rules appendix as "alethe_rules.tex"
- Add LaTeX preable to spec.tex

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