diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
index e9abc747bb..8e6bf40112 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -39,7 +39,7 @@ module LEMMAS [symbolic]
   // Word Reasoning
   // ########################
 
-    rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]
+    rule 0 <=Int size( _:List ) => true [simplification, smt-lemma]
 
     // bool2Word range & simplification
     rule 0 <=Int bool2Word(_B)             => true   [simplification]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
index 54e211ad5a..7d8ad7e05a 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -10,10 +10,8 @@ requires "lemmas/int-simplification.k"
 module EVM-OPTIMIZATIONS-LEMMAS
   imports EVM
 
-    rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                [simplification]
-    rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N)        requires I <Int #sizeWordStack(WS) [simplification]
-    rule 0 <=Int #sizeWordStack(_ , 0)    => true                                                            [simplification]
-    rule #sizeWordStack(_ , 0) <Int N     => false                        requires N <=Int 0                 [simplification]
+    rule 0 <=Int size(_:List)    => true                                                            [simplification]
+    rule size(_:List) <Int N     => false                        requires N <=Int 0                 [simplification]
 
 endmodule