You also had two requests. The first was:
TLC cannot evaluate x' = something when x is not a variable
and it would be handy to do it when x it is a sequence or record
composed of variables for example.
It appears to me that all this would achieve is allowing you to write
<<x, y, z>>' = <<A, B, C>>
(x' = A) /\ (y' = B) /\ (z' = C)
This doesn't save any significant amount of effort, and it would
encourage people to write things lik
(x + 1)' = x
which TLC couldn't possibly evaluate because it doesn't uniquely
specify the value of x'.
You also wanted to allow the suppression of the error when TLC finds
UNCHANGED x when evaluating an action in which x' has been assigned a
value. It seemed to me that in your example, this would have saved
you from writing
(x' = x) /\ UNCHANGED vars2
instead of UNCHANGED <<vars2, x>>. This doesn't seem sufficient
reason to introduce a new TLC option.