diff --git a/docs/core/tla.rst b/docs/core/tla.rst
index 89fc408..1c414a3 100644
--- a/docs/core/tla.rst
+++ b/docs/core/tla.rst
@@ -356,20 +356,29 @@ Fairness is formally defined in TLA+ as follows::
 
 In English:
 
-* ``WF_x(A)``: If it is *eventually always* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v).
-* ``SF_vars(A)``: If it is *always eventually* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v).
+* ``WF_v(A)``: If it is *eventually always* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v).
+* ``SF_v(A)``: If it is *always eventually* true that the A action *can happen* (in a way that changes v), then it *will* eventually happen (and change v).
 
 
 Fairness constraints are appended to the definition of ``Spec``. You can see this in the translation of our prior `strong fairness example <strong_fairness_spec>`::
 
   Spec == /\ Init /\ [][Next]_vars
-          /\ \A self \in Threads : SF_vars(thread(self))
+          /\ \A self \in Threads : SF_v(thread(self))
 
 (Remember, ``Spec`` defines what *counts as a valid trace*. Fairness is an additional constraint, ruling out things like infinite stutters.)
 
 Notice that by writing ``\A self: SF_vars(self)``, we're effectively making every thread fair. If we instead wrote ``\E``, we'd be saying that at least one thread is fair, but the rest may be unfair. If both those conditions are syntactically intuitive to you, I'd say you fully understand how pure TLA+ works.
 
+.. troubleshooting::
 
+  If you get
+
+    Encountered "WF_" at line X, column Y
+  or
+    Encountered "SF_" at line X, column Y
+
+  It's because you try to redefine operators (or variables) that start with ``WF_`` or ``SF_``  whereas they are already taken keywords.
+  Also make sure `VARIABLES var` is declared before using ``SF/WF_var()``.
 
 .. _fairness_status_example: