In general, action-level expressions that contain primed variables have to be boxed in [][expr]_vars or <><<expr>>_vars to ensure stuttering insensitivity. SANY will rightfully complain if you try to write an unboxed _expression_ like [](x' = 0), although this relies on syntactic pattern-matching instead of
a full stuttering sensitivity checker. ENABLED expressions are curious counterexamples to this. TLC will happily check the _expression_ ENABLED (x' = 0) as an ordinary invariant. Are ENABLED expressions thus always stuttering-insensitive?