tuples in function constructors using tlapm ?

This question seems to be answered by the documentation about partially supported features [1],
but I would like to confirm I am not doing something wrongly.

`tlapm` does not parse syntax of the form: `[<< a, b >> \in S |-> TRUE]`, so it appears to be unsupported.
`tlapm` parses `[a \in S, b \in S |-> TRUE]` and `[a, b \in S |-> TRUE]`, but it does not prove equality,
as shown in the module below. Is such syntax unsupported by `tlapm == 1.4.3`?

Does the development version of `tlapm` support syntax of this form?
Searching through the repository for usage of `|->`, I couldn't find any example of this form, except for a comment [2].

[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html
[2] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/src/oldpm/expr.ml#L81

Best regards,
ioannis

------------------------------- MODULE test --------------------------------
(* tlapm --version
   1.4.3 (build 34695)
*)
CONSTANT S

(* `tla2sany test.tla` confirms that the theorem below is well formed (p.304).

`tlapm -v -C test.tla` raises:

File "./test.tla", line 3, character 8
required expressions(s) missing before '['
File "<unknown>":
Error: Could not parse "./test.tla" successfully.
tlapm ending abnormally with Failure("Module.Parser.parse_file")
*)
(*
f == [<< a, b >> \in S |-> TRUE]
THEOREM f = [<< a, b >> \in S |-> TRUE]
    BY DEF f
*)

(* The below is well formed too, but `tlapm` raises:

Error: Could not prove or check:
         ASSUME NEW CONSTANT S,
                g == [a, b \in S |-> TRUE]
         PROVE g = [a, b \in S |-> TRUE]
*)
g == [a, b \in S |-> TRUE]
THEOREM g = [a, b \in S |-> TRUE]
    BY DEF g

(* `tlapm` can prove the following claims. *)
h == [a \in S |-> TRUE]
THEOREM h = [a \in S |-> TRUE]
    BY DEF h

p == [t \in S \X S |-> << t[1], t[0] >> ]
THEOREM p = [t \in S \X S |-> << t[1], t[0] >> ]
    BY DEF p
================================================================================