# Re: [tlaplus] Missing theorem

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