diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
index 5c8092583..0ab99545b 100644
--- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
@@ -369,11 +369,11 @@ Inv ==
     /\ IfSentPrecommitThenSentPrevote
     /\ IfSentPrecommitThenReceivedTwoThirds
     /\ AllNoEquivocationByCorrect
-    /\ PrecommitsLockValue
     /\ RelockValueIfEnoughPrevotes
     /\ AllIfValidRoundThenTwoThirds
     /\ AllValidAndLocked
     /\ AllIfValidRoundThenProposal
+    \*/\ PrecommitsLockValue
 
 \* this is the inductive invariant we like to check
 TypedInv == TypeOK /\ Inv
diff --git a/spec/light-client/accountability/TendermintAcc_004_draft.tla b/spec/light-client/accountability/TendermintAcc_004_draft.tla
index e9f3c03df..ef72b06c7 100644
--- a/spec/light-client/accountability/TendermintAcc_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAcc_004_draft.tla
@@ -495,7 +495,6 @@ EquivocationBy(p) ==
               /\ m2.src = p
               /\ m1.round = m2.round
     IN
-    \/ EquivocationIn(evidencePropose)
     \/ EquivocationIn(evidencePrevote)
     \/ EquivocationIn(evidencePrecommit)