-
Robbert Krebbers authored
Due to the new semantic invariants (!319) we no longer need to close the model (i.e. `inv_def`) to be contractive, the semantic invariant definition (i.e. `inv`) is already contractive.
0b860f2a
Due to the new semantic invariants (!319) we no longer need to close the model (i.e. `inv_def`) to be contractive, the semantic invariant definition (i.e. `inv`) is already contractive.