diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 3bc7f2de47a75fe2f834301c3b4375a8d284ba98..157732e62aeb4fa7a89989eae0ebe64ad7bb6906 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -195,7 +195,14 @@ let rec leftmost a ms =
   | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat -> begin
       let exception RetryOnUnfold in
       try (* tries to perform some rolling that do not depend on [n] *)
-        raise RetryOnUnfold
+        match ms with
+        | b::ms ->
+            let b,ms = leftmost b ms in
+            let u,us = leftmost u [] in
+            if not (F.decide (F.e_eq u b)) then raise RetryOnUnfold;
+            (*  u=b ==>  ((u^us)*^n) ^ b ^ ms  == u ^ (us^b)*^n) ^ ms *)
+            u, v_repeat (v_concat (us@[b]) (F.typeof a)) n :: ms
+        | _ -> raise RetryOnUnfold
       with RetryOnUnfold ->
         if F.decide (F.e_lt F.e_zero n) then
           (* 0<n ==> (u*^n) ^ ms ==  u ^ (u*^(n-1)) ^ ms *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
index 1a8f5dc954ad587496921c9d1021c6fccafa2bfa..44d15eeb682baf3159afe66f4dd134b42c29b074 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle
@@ -33,7 +33,7 @@ Prove: (0<=k_0) -> (k_0<(3*(length x_0)))
 ------------------------------------------------------------
 
 Lemma concat_repeat_swap:
-Prove: let a_0 = (repeat x_0 k_0) in (concat a_0 x_0)=(concat x_0 a_0)
+Prove: (repeat x_0 k_0)=(repeat x_0 k_0)
 
 ------------------------------------------------------------