Fix W.subst_l slowdown

This fixes a slowdown where the time simpl takes to simplify W.subst_l blows up exponentially with the number of local variables. (In RefinedRust, the current definition therefore makes it intractable to verify functions with 30+ local variables).

In my tests, the new definition has performed measurably better once more than 19-20 variables are involved, while performing similarly on fewer variables. Thus, there is no measurable advantage for the current RefinedC case studies, but in case someone ever verifies a function with lots of local variables, this might still be useful.