diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
index 2bcdecb27..a10695f39 100644
--- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
@@ -518,9 +518,9 @@ AgreementOnValue ==
     \A p, q \in Corr:
         /\ decision[p] /= NilDecision
         /\ decision[q] /= NilDecision
-        => \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds : 
-            /\ decision[p] = Decision(v, t1, r1)
-            /\ decision[q] = Decision(v, t2, r2)
+        => \E v \in ValidValues, t \in Timestamps, r1 \in Rounds, r2 \in Rounds :
+            /\ decision[p] = Decision(v, t, r1)
+            /\ decision[q] = Decision(v, t, r2)
 
 \* [PBTS-INV-TIME-AGR.0]
 AgreementOnTime ==