Proof fails without definition of vars.

```shell
-> % opam exec -- tlapm --version
41d03d4

-> % opam exec -- tlapm CRDT_proof.tla
(* loading fingerprints in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
(* created new ".tlacache/CRDT_proof.tlaps/CRDT_proof.thy" *)
(* fingerprints written in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
File "./CRDT_proof.tla", line 182, characters 5-6:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT Node,
                  NEW VARIABLE counter,
                  TypeOK == counter \in [Node -> [Node -> Nat]],
                  Safety == \A n, o \in Node : counter[n][n] >= counter[o][n],
                  Gossip(n, o) ==
                    LET Max(a, b) == IF a > b THEN a ELSE b
                    IN  counter'
                        = [counter EXCEPT
                             ![o] = [nodeView \in Node |->
                                   Max
                                   (counter[n][nodeView],
                                   counter[o][nodeView])]],
                  NodeAssumption == IsFiniteSet(Node),
                  DistFun(o) ==
                    [n \in Node |-> counter[n][n] - counter[o][n]],
                  TypeOK ,
                  TypeOK' ,
                  Safety ,
                  Safety' ,
                  [\E n, o \in Node : Gossip(n, o)]_vars ,
                  NEW CONSTANT v \in Node,
                  NEW CONSTANT w \in Node,
                  <1>1
           PROVE  (DistFun(v)')[w] =< DistFun(v)[w]
File "./CRDT_proof.tla", line 1, character 1 to line 354, character 77:
[ERROR]: 1/210 obligations failed.
There were backend errors processing module `"CRDT_proof"`.
 tlapm ending abnormally with Failure("backend errors: there are unproved obligations")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 446, characters 12-77
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 575, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 578, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 590, characters 8-33

-> % opam exec -- tlapm CRDT_proof.tla
(* loading fingerprints in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
(* created new ".tlacache/CRDT_proof.tlaps/CRDT_proof.thy" *)
(* fingerprints written in ".tlacache/CRDT_proof.tlaps/fingerprints" *)
File "./CRDT_proof.tla", line 1, character 1 to line 354, character 77:
[INFO]: All 210 obligations proved.
```

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

specifications/FiniteMonotonic/CRDT_proof.tla

@@ -179,7 +179,7 @@ LEMMA GossipDoesntIncreaseMeasure ==
 <1>1. CASE \E n,o \in Node : Gossip(n,o)
   <2>. ASSUME NEW v \in Node, NEW w \in Node
         PROVE  DistFun(v)'[w] <= DistFun(v)[w]
-    BY <1>1 DEF Gossip, TypeOK, Safety, DistFun
+    BY <1>1 DEF Gossip, TypeOK, Safety, DistFun, vars
   <2>. QED  
     BY SumWeaklyMonotonic, MeasureType, MeasureTypePrime, Zenon
        DEF Distance, Measure