Unified modality elimination
Currently, there are a bunch of functions eliminating/encoding certain modalities into other modalities carrying the implicit expectation that these functions are called preprocessing for interpreting over a given functor.
It would help extensibility and clarity if there was a single function representing the capabilities of all the functors handling all embeddings of one logic into another.
One possibility informally would be to have a function functor -> formula -> formula
which tries to encode a given formula for a given functor or throws an exception clearly notifying the user that the given functor doesn't support the given connective.