A little experimentation suggests that TLC cannot perform the substitution required for parametrized instantiation in expressions involving subscripts--that is, expressions of the form [A]_v, <<A>>_v, WF_v(A), and SF_v(A). Checking and possibly fixing this problem have been added to our (rather long) list of things to do. Any further information that anyone can provide about when parametrized instantiation does and doesn't work would be helpful.
Leslie