Tuple quantification should not be supported in `ASSUME NEW <<x, y>> \in S` statements

[ahelwer]

In PR #140, support for tuple quantifiers was added wherever support existed for ordinary quantification. This included adding support for the following syntax:

---- MODULE Test ----
THEOREM
  ASSUME NEW <<x, y >> \in {}
  PROVE TRUE
====

While this is a reasonable extension to the language (as is the invalid syntax NEW x, y \in S), it is not currently part of the TLA+ language standard, which only supports syntax of the form NEW x \in S here:

https://github.com/tlaplus/rfcs/blob/2a772d9dd11acec5d7dedf30abfab91a49de48b8/language_standard/grammar/TLAPlus2Grammar.tla#L243-L247

SANY also does not support it. Thus unless this extended syntax is proposed then approved as a RFC, support for it should be removed from TLAPM.

The specific offending code is the new FreshTuply variant of Expr.T.hyp (and all code that processes it):

tlapm/src/expr.mli

Lines 169 to 175 in 386cb32

	and hyp = hyp_ wrapped
	and hyp_ =
	| Fresh of hint * shape * kind * hdom
	| FreshTuply of hints * hdom
	| Flex of hint
	| Defn of defn * wheredef * visibility * export
	| Fact of expr * visibility * time

Found during work on #229. cc @johnyf

[ahelwer]

Upon further investigation TLAPM cannot actually parse the given input file. It is, however, odd that there is an AST node type variant for a construct that is not supported.

[muenchnerkindl]

@johnyf added support for tuple quantifiers such as \A <<x,y>> \in S : x = y and may have prepared the terrain for a possible extension at the level of ASSUME - PROVE, but as you say, this syntax is not part of TLA+, and I don't think we want the language to be extended in this way.