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 3dd3dfdf8b..d6ae1bb695 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
@@ -59,6 +59,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // bool2Word reasoning
   // ########################
 
+    // Reduce when the path condition only implies the argument.
+    rule [b2w-true]:  bool2Word(B) => 1 requires         B [simplification]
+    rule [b2w-false]: bool2Word(B) => 0 requires notBool B [simplification]
+
     // Range
     rule [b2w-lb]: 0 <=Int bool2Word(_)         => true [simplification, smt-lemma]
     rule [b2w-ub]:         bool2Word(_) <=Int 1 => true [simplification, smt-lemma]
diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
index ca641ac638..f0c0b8b590 100644
--- a/kevm-pyk/src/tests/integration/test_prove.py
+++ b/kevm-pyk/src/tests/integration/test_prove.py
@@ -110,6 +110,7 @@ def exclude_list(exclude_file: Path) -> list[Path]:
     'functional/lemmas-no-smt-spec.k': 'lemmas-no-smt-spec.k',
     'functional/lemmas-spec.k': 'lemmas-spec.k',
     'functional/abi-spec.k': 'abi-spec.k',
+    'functional/bool2Word-symbolic-spec.k': 'bool2Word-symbolic-spec.k',
     'functional/merkle-spec.k': 'merkle-spec.k',
     'functional/slot-updates-spec.k': 'slot-updates-spec.k',
     'functional/storageRoot-spec.k': 'storageRoot-spec.k',
diff --git a/tests/specs/functional/bool2Word-symbolic-spec.k b/tests/specs/functional/bool2Word-symbolic-spec.k
new file mode 100644
index 0000000000..07fca3ffa7
--- /dev/null
+++ b/tests/specs/functional/bool2Word-symbolic-spec.k
@@ -0,0 +1,48 @@
+requires "edsl.md"
+requires "lemmas/lemmas.k"
+
+module VERIFICATION
+    imports EDSL
+    imports LEMMAS
+
+    syntax StepSort ::= Int | Bool
+ // ------------------------------
+
+    syntax KItem ::= runLemma ( StepSort ) [symbol(runLemma)]
+                   | doneLemma( StepSort )
+ // --------------------------------------
+    rule runLemma( T ) => doneLemma( T )
+
+endmodule
+
+// Without the `b2w-true` / `b2w-false` simplification lemmas in lemmas.k,
+// claims 5-6 fail: the path condition implies but does not equate the
+// argument, so the function-rule matcher cannot discharge it without SMT.
+// With the simplification lemmas, all six claims pass.
+module BOOL2WORD-SYMBOLIC-SPEC
+    imports VERIFICATION
+
+    claim [b2w-var-true]:
+        <k> runLemma ( bool2Word(B:Bool) ) => doneLemma( 1 ) ... </k>
+        requires B
+
+    claim [b2w-var-false]:
+        <k> runLemma ( bool2Word(B:Bool) ) => doneLemma( 0 ) ... </k>
+        requires notBool B
+
+    claim [b2w-expr-eq-true]:
+        <k> runLemma ( bool2Word(X >Int Y) ) => doneLemma( 1 ) ... </k>
+        requires X >Int Y
+
+    claim [b2w-expr-eq-false]:
+        <k> runLemma ( bool2Word(X >Int Y) ) => doneLemma( 0 ) ... </k>
+        requires notBool (X >Int Y)
+
+    claim [b2w-implied-true]:
+        <k> runLemma ( bool2Word(X >=Int 0) ) => doneLemma( 1 ) ... </k>
+        requires X >Int 0
+
+    claim [b2w-implied-false]:
+        <k> runLemma ( bool2Word(X <Int 0) ) => doneLemma( 0 ) ... </k>
+        requires X >Int 0
+endmodule