Mea culpa. One can no longer write a SV!< b in TLA+. Version 2 of TLA+ allows this _expression_ to be written in the more readable form SV!<(a, b). I had forgotten that it also disallows the previous syntax. So, this is a bug in the Decompose Proof command.
Leslie