diff --git a/spec/light-client/accountability/TendermintAccInv_004_draft.tla b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
index 0ab99545b..28c63cb3f 100644
--- a/spec/light-client/accountability/TendermintAccInv_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAccInv_004_draft.tla
@@ -295,12 +295,15 @@ PrecommitsLockValue ==
   \A r \in Rounds:
     \A v \in ValidValues:
       \/ LET Precommits == {
-            m \in msgsPrecommit[r]: m.id = v /\ m.src \in Corr
+            m \in msgsPrecommit[r] \intersect evidencePrecommit:
+              m.id = v /\ m.src \in Corr
          }
          IN
          Cardinality(Senders(Precommits)) < THRESHOLD1
       \/ \A fr \in Rounds, w \in Values:
-          LET Prevotes == { m \in msgsPrevote[fr]: m.id = w } IN
+          LET Prevotes == {
+            m \in msgsPrevote[fr] \intersect evidencePrevote: m.id = w
+          } IN
           (fr > r /\ w /= v) => (Cardinality(Senders(Prevotes)) < THRESHOLD2)
 
 \* Another lemma by Josef Widder:
diff --git a/spec/light-client/accountability/TendermintAcc_004_draft.tla b/spec/light-client/accountability/TendermintAcc_004_draft.tla
index ef72b06c7..d0bce2b2e 100644
--- a/spec/light-client/accountability/TendermintAcc_004_draft.tla
+++ b/spec/light-client/accountability/TendermintAcc_004_draft.tla
@@ -382,7 +382,8 @@ UponQuorumOfPrecommitsAny(p) ==
       LET Committers == { m.src: m \in MyEvidence } IN
       \* compare the number of the unique committers against the threshold
       /\ Cardinality(Committers) >= THRESHOLD2 \* line 47
-      /\ evidencePrecommit' = MyEvidence \union evidencePrecommit
+      \*/\ evidencePrecommit' = MyEvidence \union evidencePrecommit
+      /\ UNCHANGED evidencePrecommit
       /\ round[p] + 1 \in Rounds
       /\ StartRound(p, round[p] + 1)
       /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
@@ -434,7 +435,8 @@ OnQuorumOfNilPrevotes(p) ==
   /\ step[p] = "PREVOTE"
   /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilValue) } IN
     /\ Cardinality(PV) >= THRESHOLD2 \* line 36
-    /\ evidencePrevote' = PV \union evidencePrevote
+    \*/\ evidencePrevote' = PV \union evidencePrevote
+    /\ UNCHANGED evidencePrevote
     /\ BroadcastPrecommit(p, round[p], Id(NilValue))
     /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
     /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
@@ -455,9 +457,10 @@ OnRoundCatchup(p) ==
             Src(EvPropose) \union Src(EvPrevote) \union Src(EvPrecommit)
         IN
         /\ Cardinality(Faster) >= THRESHOLD1
-        /\ evidencePropose' = EvPropose \union evidencePropose
-        /\ evidencePrevote' = EvPrevote \union evidencePrevote
-        /\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
+        /\ UNCHANGED <<evidencePropose, evidencePrevote, evidencePrecommit>>
+        \*/\ evidencePropose' = EvPropose \union evidencePropose
+        \*/\ evidencePrevote' = EvPrevote \union evidencePrevote
+        \*/\ evidencePrecommit' = EvPrecommit \union evidencePrecommit
         /\ StartRound(p, r)
         /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
                       validRound, msgsPropose, msgsPrevote, msgsPrecommit>>
@@ -495,6 +498,7 @@ EquivocationBy(p) ==
               /\ m2.src = p
               /\ m1.round = m2.round
     IN
+    \/ EquivocationIn(evidencePropose)
     \/ EquivocationIn(evidencePrevote)
     \/ EquivocationIn(evidencePrecommit)