This is a computer modern clone with unicode support.  This
hopefully fixes the error in the CI.

- 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

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

It was used in a few places to represent complementary literals,
but is mostly used to represent vectors of terms, variables.  This
commit removes the usage for complementary literals.  The few
places that used it now define the complement manually.

Also introduces the notation of $\bar x_n$ which is used in several places.