Prove more of progress; fix SIfV definition; account for ae_fork in step

Previously, step relations didn't account for the fact that the end of
the threads may change after evaluating an active expression. If that
active expression was a fork, then t' would change.

The definition of SIfV no longer allows EConst 0 to step to the
true branch. Previously, EConst 0 could step to both the true and
false case.
Changed variable naming for lists of threads to be consistent.