Fix kompile warnings. (#1001)

Author: anvacaru

src/kontrol/kdist/keccak.md

@@ -33,8 +33,8 @@ module KECCAK-LEMMAS
 4. The result of a `keccak` is assumed not to fall too close to the edges of its official range. This accounts for the shifts added to the result of a `keccak` when accessing storage slots, and is a hypothesis made by the ecosystem.
 
 ```k
-    rule BOUND:Int <Int keccak(B:Bytes) => true requires BOUND <=Int 32             [simplification, concrete(BOUND)]
-    rule keccak(B:Bytes) <Int BOUND:Int => true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)]
+    rule BOUND:Int <Int keccak(_B:Bytes) => true requires BOUND <=Int 32             [simplification, concrete(BOUND)]
+    rule keccak(_B:Bytes) <Int BOUND:Int => true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)]
 ```
 
 5. `keccak` is injective: that is, if `keccak(A)` equals `keccak(B)`, then `A` equals `B`.

src/kontrol/kdist/kontrol_lemmas.md

@@ -61,7 +61,7 @@ module KONTROL-AUX-LEMMAS
       requires C +Int D ==Int 0 [simplification, preserves-definedness]
 
     // modInt
-    rule (X *Int Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]
+    rule (X *Int _Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]
 
     // >>Int
     rule [shift-to-div]: X >>Int N => X /Int (2 ^Int N)
@@ -197,9 +197,9 @@ module KONTROL-AUX-LEMMAS
     rule KI:KItem in ListItem(KJ:KItem) => KI ==K KJ [simplification]
 
     // Recursive list membership check for lists with multiple elements
-    rule KI:KItem in (ListItem(KI) Rest) => true [simplification]
-    rule KI:KItem in (ListItem(KJ) Rest) => KI in Rest [simplification]
-    rule KI:KItem in .List => false [simplification]
+    rule KI:KItem in (ListItem(KI) _REST) => true [simplification]
+    rule KI:KItem in (ListItem(KJ) REST) => KI in REST requires KI =/=K KJ [simplification]
+    rule _KI:KItem in .List => false [simplification]
 
 endmodule
 ```