In order to make the lower-level "interface" of ReLoC more clear, it could be worth hiding the
we can just define new
\Mapsto as a conjunction of
spec_ctx and the old
It might be worth incorporating this into the
ext_lp branch, depending on whether we do something similar there.