I've used this variant and thank you it works.
Also intriguing is the following fact.
This lemma is obvious according to TLAPS:
ASSUME NEW S, NEW T \in S, NEW U \in S
PROVE << T , U >> \in S \X S
And it is true it is consistent with the semantics of a tuple
described by "Specifying Systems".
But this one is unprovable (automatically I mean):
ASSUME NEW S, NEW T \in S
PROVE << T >> \in S
--
FL