Most notably, there is no need to internalize stuff into the logic
as it follows from generic lemmas for discrete COFEs/CMRAs.