diff --git a/prover/prover.md b/prover/prover.md
index f9f657136..b198676cb 100644
--- a/prover/prover.md
+++ b/prover/prover.md
@@ -31,6 +31,8 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "direct-proof"
                     | "check-lhs-constraint-unsat"
                     | "smt" | "smt-z3" | "smt-cvc4" | "smt-debug"
+                    | "just-left-unfold-Nth" "(" Int ")"
+                    | "just-right-unfold-Nth" "(" Int ")"
                     | "left-unfold" | "left-unfold-Nth" "(" Int ")"
                     | "right-unfold" | "right-unfold-Nth" "(" Int "," Int ")" | "right-unfold" "(" Symbol ")"
                     | "right-unfold-all"  "(" "bound" ":" Int ")"
diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md
index 543a12faa..e69f5fadb 100644
--- a/prover/strategies/unfolding.md
+++ b/prover/strategies/unfolding.md
@@ -62,6 +62,63 @@ module STRATEGY-UNFOLDING
     => getUnfoldables(P) ++Patterns getUnfoldables(REST)
 ```
 
+### Just Right Unfold
+
+```k
+
+  rule <strategy> just-right-unfold-Nth(M)
+               => just-right-unfold-Nth-#1(M, getUnfoldables(RHS))
+                  ...
+       </strategy>
+       <claim> \implies(\and(LHS), RHS) </claim>
+
+  syntax Strategy ::= "just-right-unfold-Nth-#1"  "(" Int "," Patterns ")"
+                    | "just-right-unfold-Nth-#2"  "(" Pattern "," Pattern ")"
+
+
+  rule <strategy> just-right-unfold-Nth-#1(M, PS)
+               => just-right-unfold-Nth-#2(getMember(M, PS), unfold(getMember(M, PS)))
+                  ...
+       </strategy>
+  requires 0 <=Int M andBool M <Int getLength(PS)
+
+  rule <claim> \implies(LHS, RHS => subst(RHS, PATTERN, BODY)) </claim>
+       <strategy> just-right-unfold-Nth-#2(PATTERN, BODY)
+               => noop
+                  ...
+       </strategy>
+```
+
+
+### Just Left Unfold Nth
+
+Just unfolds the Nth predicate on the LHS.
+
+```k
+  rule <strategy> just-left-unfold-Nth(M)
+               => just-left-unfold-Nth-#1(M, getUnfoldables(LHS))
+                  ...
+       </strategy>
+       <claim> \implies(\and(LHS), RHS) </claim>
+
+  syntax Strategy ::= "just-left-unfold-Nth-#1"  "(" Int "," Patterns ")"
+                    | "just-left-unfold-Nth-#2"  "(" Pattern "," Pattern ")"
+
+
+  rule <strategy> just-left-unfold-Nth-#1(M, PS)
+               => just-left-unfold-Nth-#2(getMember(M, PS), unfold(getMember(M, PS)))
+                  ...
+       </strategy>
+  requires 0 <=Int M andBool M <Int getLength(PS)
+
+  rule <claim> \implies(LHS => subst(LHS, PATTERN, BODY), RHS) </claim>
+       <strategy> just-left-unfold-Nth-#2(PATTERN, BODY)
+               => noop
+                  ...
+       </strategy>
+
+```
+
 ### Left Unfold (incomplete)
 
 ```k