Your property expresses that a condition P is stable, i.e. once it is true, it remains true forever. The standard way to prove this is to show
Inv => (P /\ [Next]_vars => P’) or equivalently Inv /\ P /\ [Next]_vars => P'
for a suitable invariant Inv (we are only interested in stability for all reachable states, the invariant serves to characterize those). The conclusion
[]Inv /\ [][Next]_vars => [](P => []P)
follows by simple (propositional) temporal logic. This is exactly what the quiescence proof in the example does (where TypeOK plays the role of the invariant).
As you say, your case is a little more complicated because P is not purely propositional but a first-order predicate with a parameter x. However, that parameter is bound outside the temporal-logic formula, so we can introduce a fresh parameter in the context and then pretend that P has no free variable anymore. (In the PM, we call this technique ``coalescing’’, you can find a pretty technical description of it at [1].)
Your proof should then look somewhat like this:
THEOREM Spec => \A t \in TaskId : [](t \in FinalizedTask => [](t \in FinalizedTask))
<1>. SUFFICES
ASSUME NEW t \in TaskId
PROVE Spec => [](t \in FinalizedTask => [](t \in FinalizedTask))
OBVIOUS
<1>1. Inv /\ t \in FinalizedTask /\ [Next]_vars => (t \in FinalizedTask)’
\* here you prove a non-temporal property
<1>2. QED
BY <1>1, Invariant, PTL DEF Spec
In the justification of the QED step, "Invariant" refers to a previously proved theorem Spec => []Inv. The definition of Spec must be used in order to relate the formula Spec to [Next]_vars, which appears in <1>1.
If you have trouble making this work, feel free to contact me off-list.
Hope this helps,
Stephan