Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/. And here is another encoding for model checking: https://dl.acm.org/doi/10.1145/3360549