diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md
index abef7988e..366c15b46 100644
--- a/prover/lang/kore-lang.md
+++ b/prover/lang/kore-lang.md
@@ -141,12 +141,15 @@ only in this scenario*.
 ```k
   syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)]
   syntax SetVariable ::= SharpName [klabel(setVariable)]
+  syntax Context ::= VariableName "[" Pattern "]" [klabel(context)]
   syntax Pattern ::= Int
                    | Variable
                    | SetVariable
                    | Symbol
                    | Symbol "(" Patterns ")"                    [klabel(apply)]
 
+                   | Context
+
                    | "\\top"    "(" ")"                         [klabel(top)]
                    | "\\bottom" "(" ")"                         [klabel(bottom)]
                    | "\\equals" "(" Pattern "," Pattern ")"     [klabel(equals)]
@@ -359,8 +362,8 @@ module KORE-HELPERS
 
   rule getReturnSort(\exists{Vs} P) => getReturnSort(P)
 
-  syntax Sort ::= "TopSort"         [token]
-                | "BottomSort"      [token]
+  syntax UpperName ::= "TopSort"         [token]
+                     | "BottomSort"      [token]
 
   syntax Sort ::= unionSort(Sort, Sort) [function]
   rule unionSort(TopSort, S) => TopSort
@@ -833,10 +836,10 @@ Simplifications
 
   // TODO: This should use an axiom, similar to `functional` instead: `axiom predicate(P)`
   rule isPredicatePattern(S:Symbol(ARGS)) => true
-    requires getReturnSort(S(ARGS)) =/=K Heap
+    requires getReturnSort(S(ARGS)) ==K Bool
 
   rule isPredicatePattern(S:Symbol(ARGS)) => false
-    requires getReturnSort(S(ARGS)) ==K Heap
+    requires getReturnSort(S(ARGS)) =/=K Bool
   rule isPredicatePattern(emp(.Patterns)) => false
   rule isPredicatePattern(\exists{Vs} P) => isPredicatePattern(P)
   rule isPredicatePattern(\forall{Vs} P) => isPredicatePattern(P)
@@ -857,6 +860,8 @@ Simplifications
   rule isSpatialPattern(\or(_)) => false
   rule isSpatialPattern(S:Symbol(ARGS)) => true
     requires S =/=K sep andBool getReturnSort(S(ARGS)) ==K Heap
+  rule isSpatialPattern(S:Symbol(ARGS)) => false
+    requires getReturnSort(S(ARGS)) =/=K Heap
   rule isSpatialPattern(#hole { Bool }) => false
   rule isSpatialPattern(#hole { Heap }) => true
   rule isSpatialPattern(V:VariableName { Heap }) => true
@@ -918,6 +923,7 @@ Simplifications
   rule hasImplicationContext(\functionalPattern(P)) => hasImplicationContext(P)
   rule hasImplicationContext(\exists{ _ } P ) => hasImplicationContext(P)
   rule hasImplicationContext(\forall{ _ } P ) => hasImplicationContext(P)
+  rule hasImplicationContext(\mu X . P) => hasImplicationContext(P)
   rule hasImplicationContext(implicationContext(_, _)) => true
   rule hasImplicationContextPs(.Patterns) => false
   rule hasImplicationContextPs(P, Ps)
diff --git a/prover/strategies/core.md b/prover/strategies/core.md
index b82c12246..3a2b3cefb 100644
--- a/prover/strategies/core.md
+++ b/prover/strategies/core.md
@@ -290,8 +290,8 @@ Internal strategy used to implement `or-split` and `and-split`.
 `rhs-top` evaluates to success if the right hand side is top
 
 ```k
-  rule <k> \implies(LHS, \exists{.Patterns} \and(.Patterns)) </k>
-       <strategy> rhs-top => success ... </strategy>
+  rule <claim> \implies(LHS, \exists{.Patterns} \and(.Patterns)) </claim>
+       <k> rhs-top => success ... </k>
 ```
 
 If-then-else-fi strategy is useful for implementing other strategies:
diff --git a/prover/strategies/knaster-tarski.md b/prover/strategies/knaster-tarski.md
index 19f6ca292..82beb6ebe 100644
--- a/prover/strategies/knaster-tarski.md
+++ b/prover/strategies/knaster-tarski.md
@@ -384,7 +384,9 @@ Move #holes to the front
 ```
 
 ```k
-  rule <claim> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { SORT }, _) , _ ) , _ ) , _ ) </claim>
+  rule <claim> \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ ) </claim>
+       <k> normalize-implication-context => noop ... </k>
+  rule <claim> \implies(\and( S:Symbol(\forall { UNIVs } implicationContext( \and(#hole { TopSort }, _) , _ )) , _ ) , _ ) </claim>
        <k> normalize-implication-context => noop ... </k>
   rule <claim> \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ ) </claim>
        <k> normalize-implication-context => noop ... </k>
@@ -496,6 +498,50 @@ of heaps.
        </k>
 ```
 
+```k
+  syntax UpperName ::= "#rest" [token]
+  rule <claim> \implies( \and( S:Symbol ( \forall { UNIVs }
+                                      implicationContext(\and(CTXLHS), CTXRHS)
+                                    )
+                         , LHS:Patterns
+                         )
+                   , RHS:Pattern
+                   )
+       </claim>
+       <k> kt-collapse
+               => with-each-match( #matchAssoc( terms:     S( #hole { TopSort } )
+                                              , pattern:   #rest[CTXLHS]
+                                              , variables: #rest { TopSort }
+                                              , subst:     .Map
+                                              , rest:      .Patterns
+                                              )
+                                 , kt-collapse
+                                 , kt-collapse-no-match
+                                 )
+                  ...
+       </k>
+```
+
+```k
+  rule <claim> \implies( \and( S:Symbol ( \forall { .Patterns }
+                                      implicationContext( \and(_), CTXRHS )
+                                    )
+                         , LHS:Patterns
+                         )
+                   , RHS:Pattern
+                   )
+         => \implies( \and( subst({SUBST[#rest { TopSort }]}:>Pattern, #hole { TopSort }, CTXRHS)
+                          , LHS
+                          )
+                    , RHS
+                    )
+       </claim>
+       <k> ( #matchResult(subst: SUBST, rest: .Patterns) ~> kt-collapse )
+               => noop
+                  ...
+       </k>
+```
+
 In the context of the heuristics we implement, this becomes the following, where
 REST is obtained via matching:
 
diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
index e79c02178..052f8fd31 100644
--- a/prover/strategies/matching.md
+++ b/prover/strategies/matching.md
@@ -91,6 +91,19 @@ Work around OCaml not producing reasonable error messages:
 Recurse over assoc-only constructors (including `pto`):
 
 ```k
+  // TODO: matching over context patterns
+  rule #matchAssoc( terms:     S:Symbol(T), .Patterns
+                  , pattern:   V[T], .Patterns
+                  , variables: Vs
+                  , subst:     SUBST
+                  , rest:      REST
+                  )
+    => #matchResult( subst: SUBST V { getReturnSort(S(T)) } |-> S( #hole { getReturnSort(T) })
+                   , rest: .Patterns
+                   )
+     , .MatchResults
+    requires V { getReturnSort(S(T)) } in Vs
+
   // Base case
   rule #matchAssoc( terms:     .Patterns
                   , pattern:   .Patterns
@@ -679,15 +692,15 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
 If the RHS is empty, we have nothing to do
 
 ```k
-    rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
-         <strategy> patterns-equal => noop ... </strategy>
+    rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
+         <k> patterns-equal => noop ... </k>
 ```
 
 Remove any patterns on the RHS that match a pattern on the LHS:
 
 ```k
-    rule <k> \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) </k>
-         <strategy> patterns-equal
+    rule <claim> \implies(\and(LHS), \exists{Vs} \and(RHS, REST)) </claim>
+         <k> patterns-equal
                  => with-each-match( #match( terms: LHS
                                            , pattern: RHS
                                            , variables: .Patterns
@@ -695,21 +708,21 @@ Remove any patterns on the RHS that match a pattern on the LHS:
                                    , patterns-equal
                                    )
                     ...
-         </strategy>
-    rule <k> \implies(LHS, \exists{ Vs } \and(RHS, REST))
-              => \implies(LHS, \exists{ Vs } \and(REST))
          </k>
-         <strategy> #matchResult(subst: .Map , rest: .Patterns)
+    rule <claim> \implies(LHS, \exists{ Vs } \and(RHS, REST))
+              => \implies(LHS, \exists{ Vs } \and(REST))
+         </claim>
+         <k> #matchResult(subst: .Map , rest: .Patterns)
                  ~> patterns-equal
                  => patterns-equal
                     ...
-         </strategy>
+         </k>
 
-    rule <strategy> #matchResult(subst: .Map , rest: P, Ps)
-                 ~> patterns-equal
-                 => fail
-                    ...
-         </strategy>
+    rule <k> #matchResult(subst: .Map , rest: P, Ps)
+          ~> patterns-equal
+          => fail
+             ...
+         </k>
 ```
 
 If the RHS has no spatial part, then there is nothing to do:
diff --git a/prover/strategies/simplification.md b/prover/strategies/simplification.md
index b9fa81aa6..623be3f6d 100644
--- a/prover/strategies/simplification.md
+++ b/prover/strategies/simplification.md
@@ -342,6 +342,8 @@ Bring predicate constraints to the top of a term.
 
   syntax Pattern ::= #liftConstraints(Pattern) [function]
   syntax Patterns ::= #liftConstraintsPs(Patterns) [function]
+  // rule #liftConstraints(S:Symbol(\and(P1, P2, Ps), ARGs)) => #liftConstraints(\and(S(P1, ARGs), S(\and(P2, Ps), ARGs)))
+  // rule #liftConstraints(S:Symbol(\and(P, .Patterns), ARGs)) => #liftConstraints(\and(S(P, ARGs)))
   rule #liftConstraints(\and(Ps)) => \and(#liftConstraintsPs(Ps))
   rule #liftConstraintsPs(.Patterns) => .Patterns
   rule #liftConstraintsPs(sep(\and(.Patterns), .Patterns), REST) => #liftConstraintsPs(REST)
diff --git a/prover/t/ltl/until-implies-eventually.kore b/prover/t/ltl/until-implies-eventually.kore
index 9dd34b605..d1cc74b68 100644
--- a/prover/t/ltl/until-implies-eventually.kore
+++ b/prover/t/ltl/until-implies-eventually.kore
@@ -37,4 +37,6 @@ right-unfold-Nth(0, 1)
 phi-implies-phi
 */
 
-strategy normalize . kt . right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top
+strategy normalize . kt . ( ( right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top )
+                          | ( right-unfold-Nth(0, 1) . normalize . lift-constraints . wait . patterns-equal . rhs-top )
+                          )
diff --git a/prover/t/unit/match-assoc.k b/prover/t/unit/match-assoc.k
index 6696afbb9..1d52f5dd4 100644
--- a/prover/t/unit/match-assoc.k
+++ b/prover/t/unit/match-assoc.k
@@ -110,6 +110,7 @@ module TEST-MATCH-ASSOC
   // Match constructor against variable
   rule test("match-assoc", 9)
     => symbol pto ( Loc, Data ) : Heap
+       symbol c ( Data ) : Data
        assert( #error("Constructors do not match")
              , .MatchResults
             == #matchAssoc( terms:     X0 { Loc }, Y0 { Data }
@@ -120,4 +121,19 @@ module TEST-MATCH-ASSOC
                           )
              )
        .Declarations
+  // Match multiple occurances of a variable
+  rule test("match-assoc", 10)
+    => symbol c ( Data ) : Data
+       assert( #matchResult( subst:    X0 |-> c( #hole { Data } )
+                           , rest:     .Patterns
+                           )
+             , .MatchResults
+            == #matchAssoc( terms:     c( W { Data } )
+                          , pattern:   X0[W { Data }]
+                          , variables: X0 { Data }
+                          , subst:     .Map
+                          , rest:      .Patterns
+                          )
+             )
+       .Declarations
 endmodule