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