Concrete implementation of ==K hook; internal simplification rules

[ana-pantilie]

Needs #1772
Needs #1774

Fixes #1648

• ==K hook is evaluated for constructor-like input only
• adds internal simplification rules for bool and kequal
• fixes unit tests
• adds new integration test not-kequal (reduced example from evm-semantics)

---

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock

[ttuegel]

We should make the new integration tests independent of the frontend, so that we do not have to wait for the frontend release to pass before we can merge this pull request. The evm-semantics regression tests in this repository do the same thing. There is a script which generates the Kore files from the K files, and we commit the Kore files into the repository. You should make a copy of that script and modify it for the new tests. For each test, the script should invoke kollect test-name kprove ... (fill in ... with the arguments to kprove). Then, you would run the script with the correct frontend version on your PATH and with KORE pointing to your clone of the Kore repository. We should also commit the K source files to the repository (so that the tests can be re-generated) but these should go in a subdirectory so that the Makefile doesn't try to run them automatically. (It will run the generated tests instead.)