Upstream dependencies for Infinite Descent section 2.1

[pimotte]

This is the upstreaming of some work of @cyborggeneraal.

Stuff that was needed:

• Avoid sumbool and sigma type notations, as they conflict with set notation
• Magic with notation to make stuff work

TODO:

• Make characterizations work both ways (@jim-portegies Is this just a matter of making it an if-and-only-if? How should I add it in the database?)
• Write more tests

[jim-portegies]

As an answer to the question above: I think we often add one side of the implication to the automation system. But sometimes we even add both. But it may not be the best design, as it may create loops. At the same time, I think our automation system has some detection of loops.