diff --git a/specifications/FiniteMonotonic/CRDT_proof.tla b/specifications/FiniteMonotonic/CRDT_proof.tla
index 7e4d016a..6961f8d0 100644
--- a/specifications/FiniteMonotonic/CRDT_proof.tla
+++ b/specifications/FiniteMonotonic/CRDT_proof.tla
@@ -339,7 +339,7 @@ THEOREM OGLiveness == OGSpec => <>(\A n, o \in Node : counter[n] = counter[o])
 <1>2. ASSUME NEW m \in Nat,
              \A k \in 0 .. (m-1) : S(k)
       PROVE  S(m)
-  BY <1>1
+  BY <1>1, <1>2
 <1>3. \A m \in Nat : S(m)
   <2>. HIDE DEF S
   <2>. QED  BY <1>2, GeneralNatInduction, Isa