Reading chapter 17 of Specifying Systems, I now better understand TLA+'s evaluation strategy, so I guess my question becomes, is there a way to force the evaluation of an _expression_ before the beta-reduction so that it is no longer subject to priming, as the prime operator (when applied to an _expression_) seems to be sensitive to a specific evaluation strategy?
Ron