Rigid and flexible variables

I've just read Leslie Lamport's "Temporal Logic of Actions" ACM Transactions on Programming Languages and Systems, 1994:

http://dl.acm.org/citation.cfm?id=177726

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-actions.pdf

(I suppose this article is an exact description of what is implemented currently by TLA+ and TLAPS).

And I just wonder: when in a proof the goal is:

\A x \in A : P (A a set, P an action),

and then you have the step:

TAKE x \in A,

what is the status of x?

I bet for a rigid variable (see p. 6). (The other possibility would be a variable neither rigid nor flexible but I don't think so.)

I think the "only" difference between a flexible and a rigid variable only consists in their semantic interpretation (p. 34)
"sequences of state functions" versus "elements of Val" and in the way of quantifying them: \AA \EE versus \A \E.

--
FL