First of all, Stephan is correct that the [] should be added to [Next]_vars rather than removed from []Inv.
Second, I see that the proof actually was rerun through the provers in November 2013 and the error
corrected in my own copy. However, I failed to update the version on the Web. The proofs need additional
changes to keep up with changes to the prover. I will try to get new versions of those files on the Web
as soon as I can.
Leslie