tuple declarations will soon be supported, apologies for the long wait!
However, in your example, they are unnecessary: you can simply write
LEMMA LEM1 == ASSUME NEW S1, NEW S2,
NEW Set \in SUBSET (S1 \X S2),
NEW p \in Set
PROVE p \in S1
which is equivalent, and proved.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BD8B3B19-69C6-419A-AD38-5AA5228F5099%40gmail.com.