diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
index 1a3e6b37a3..00ad215864 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
@@ -228,7 +228,7 @@ module BYTES-SIMPLIFICATION [symbolic]
       [simplification]
 
     rule [memUpdate-concat-in-left]: (B1 +Bytes B2) [ S := B ] => (B1 [ S := B ]) +Bytes B2
-      requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1)
+      requires 0 <=Int S andBool S +Int lengthBytes(B) <Int lengthBytes(B1)
       [simplification(40)]
 
     rule [memUpdate-concat-in-right]: (B1 +Bytes B2) [ S := B ] => B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ])
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index bd5acfe8ae..58f2fb0983 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -361,6 +361,11 @@ module LEMMAS-SPEC
       <k> runLemma( #range (#buf(8, X:Int), -3, _:Int) ) => doneLemma( .Bytes ) ... </k>
       requires 0 <=Int X andBool X <Int pow64
 
+    claim [range-39]:
+      <k> runLemma( b"\xaa" ==K #range ( ( BYTES:Bytes +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) [ ( lengthBytes ( BYTES:Bytes ) /Int 2 ) := b"\xaa" ] , ( lengthBytes ( BYTES:Bytes ) /Int 2 ) , 1 ) )
+            => doneLemma(true) ... </k>
+      requires lengthBytes ( BYTES:Bytes ) <Int 32
+
  // #buf simplification
  // -------------------
     claim [bufExtractPadding]: <k> runLemma ( #asWord ( ( #range( #buf ( 32 , X ), 0, 28 ) ):Bytes ) ) => doneLemma ( 0 ) ... </k> requires #rangeUInt(32, X)