HOL improvements

[mezpusz]

This PR contains the following improvements towards HOL in master:

1. a couple of HOL inferences (some of them in a cleaned up way), and unit testing for most of them,
2. a fix for beta-eta simplification (it wasn't working on the top-level term),
3. non-selection of flex-flex pairs (complemented by a flex-flex simplification inference that gets rid of them),
4. a new heuristic of function elimination for arrow types terms,
5. disabling unifying with or superposing/rewriting into some lambda terms via superposition and demodulation to avoid some DB indices popping up unbound,
6. a check that crashes Vampire if we notice a DB index popping up unbound for the rest.

Regression over FOL TPTP with Discount/Otter actually shows 3, resp. 5 problems gained (I will check these), while regression over HOL TPTP with Discount/Otter shows ~1000 problems gained over master (and <100 lost due to divergence in saturation or because of the unsoundness caused by the unbound DB indices). We also crash now on a few hundred problems. I hope this chaos will all go away once more features and fixes get merged.

[quickbeam123]

Doesn't this change affect plain first order paths through the code?

[mezpusz]

It is called from first-order paths, too, but the default implementation kicks in, which just checks ts == transformed, so the extra condition is always true for those implementations.