I highly recommend learning TLA+ before writing any papers with math involving set logic (foreach, exists, etc), if only to teach you standard mathematical syntax for those things (like “{ s \in S : \A t \in s : func(t) }“, which is valid TLA, and will also emit a human readable formula if pasted into Latex).

This would have saved me tons of work in hindsight.