diff --git a/specifications/FiniteMonotonic/CRDT_proof.tla b/specifications/FiniteMonotonic/CRDT_proof.tla
index 6961f8d0..246420ab 100644
--- a/specifications/FiniteMonotonic/CRDT_proof.tla
+++ b/specifications/FiniteMonotonic/CRDT_proof.tla
@@ -305,7 +305,7 @@ THEOREM OGLiveness == OGSpec => <>(\A n, o \in Node : counter[n] = counter[o])
                       => <> \E k \in 0 .. (m-1) : P(k)
           OBVIOUS
         <5>1. TypeOK /\ C(u,v) => ENABLED <<Gossip(u,v)>>_vars
-          BY EnabledGossip
+          BY EnabledGossip, ExpandENABLED DEF Gossip, vars, C
         <5>2. /\ TypeOK /\ TypeOK' /\ Safety /\ Safety'
               /\ \E k \in 0 .. m : P(k)
               /\ <<Gossip(u,v)>>_vars