Improve the `eq` module

- Make it possible to install immediate equations (maybe both, normalized and non-normalized)
- There should be a way to locally use an equation.
- There should be a way to block an equation that's already installed.
- It would be nice if we can have multiple equality checkers at the same time, apart from the default one.