Rules about enter-scope.
We do not provide any theorem about enter-scope, as it is part of the canonical representation of computation states.