What you want to check is a temporal safety property of your spec. The canonical way to write a safety property in TLA+ is in the form
(*) I /\ [][A]_v
where I is a state predicate, A an action, and v a state function. For example, the invariance formula []Inv can be written as
Inv /\ [][Inv']_Inv
Your formula T2 has the form (*), where I equals TRUE. TLC can generate the set of all possible behaviors allowed by (*) only when I, A, and v have a very special form. Not coincidentally, this is a natural form in which to describe algorithms and high-level designs of systems--which is why TLA+ and TLC are useful. TLC can check that a set of behaviors it can generate all satisfy (*) on a much larger class of formulas I, A, and v. It just has to be able to compute I, A, and v on all states or pairs of states that occur in that set of behaviors.
Leslie