diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
index d920597b3..c8caa5f58 100644
--- a/prover/strategies/matching.md
+++ b/prover/strategies/matching.md
@@ -702,10 +702,11 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
     //      </strategy>
     //   requires RSPATIAL -Patterns REST ==K .Patterns
 
-    rule <claim> \implies(LHS, RHS) </claim>
+    rule <claim> \implies(\and(LHS), RHS)
+              => \implies(\and(LHS -Patterns getSpatialPatterns(LHS)), RHS)
+         </claim>
          <strategy> spatial-patterns-match => noop ... </strategy>
-       requires isPredicatePattern(LHS)
-        andBool isPredicatePattern(RHS)
+       requires isPredicatePattern(RHS)
 ```
 
 ### Footprint Analysis