diff --git a/NEWS b/NEWS
index 5c2e9da88..8c1679c65 100644
--- a/NEWS
+++ b/NEWS
@@ -130,6 +130,13 @@ New in spot 2.5.3.dev  (not yet released)
     the resulting TGBA makes it more likely that simulation-based
     reductions will reduce it.
 
+  - The LTL simplification routine learned the following reductions,
+    where f is any formula, and q is a "suspendable" formula (a.k.a.
+    both a pure eventuality and purely universal).
+
+      q R Xf = X(q R f)
+      q U Xf = X(q U f)
+
   Python:
 
   - New spot.jupyter package.  This currently contains a function for
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 511159db4..5cdde599a 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1669,22 +1669,22 @@ notation to distinguish the class of subformulas:
 \begin{center}
 \begin{tabular}{rl}
 \toprule
-$f,\,f_i,\,g,\,g_i$ & any PSL formula \\
-$e,\,e_i$           & a pure eventuality \\
-$u,\,u_i$           & a purely universal formula \\
+$f,\,f_i,\,g,\,g_i$ & any PSL formula                                  \\
+$e,\,e_i$           & a pure eventuality                               \\
+$u,\,u_i$           & a purely universal formula                       \\
 $q,\,q_i$           & a pure eventuality that is also purely universal \\
 \bottomrule
 \end{tabular}
 \end{center}
 
 \begin{align*}
-  \F e        & \equiv e            & f \U e         & \equiv e                & e \M g        & \equiv e\AND g & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\
-  \F(u)\OR q  & \equivEU \F(u\OR q) & f \U (g\OR e)  & \equivEU (f \U g)\OR e  & f\M (g\AND u) & \equivEU (f \M g)\AND u                                \\
-              &                     & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q                                \\
-  \G u        & \equiv u            & u \W g         & \equiv u\OR g           & f \R u        & \equiv u       & e_1 \W e_2 & \equiV (\G e_1) \OR e_2  \\
-  \G(e)\AND q & \equiv \G(e\AND q)  & f \W (g\OR e)  & \equivEU (f \W g)\OR e  & f\R (g\AND u) & \equivEU (f \R g)\AND u                                \\
-  \X q        & \equiv q            & q \AND \X f    & \equivNeu \X(q \AND f)  & q\OR \X f     & \equivNeu \X(q \OR f)                                  \\
-              &                     & \X(q \AND f)   & \equivEU q \AND \X f    & \X(q \OR f)   & \equivEU q\OR \X f                                     \\
+  \F e        & \equiv e             & f \U e         & \equiv e                & e \M g        & \equiv e\AND g          & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\
+  \F(u)\OR q  & \equivNeu \F(u\OR q) & f \U (g\OR e)  & \equivEU (f \U g)\OR e  & f\M (g\AND u) & \equivEU (f \M g)\AND u & q \U\X f   & \equiv \X(q \U f)        \\
+              &                      & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q                                         \\
+  \G u        & \equiv u             & u \W g         & \equiv u\OR g           & f \R u        & \equiv u                & e_1 \W e_2 & \equiV (\G e_1) \OR e_2  \\
+  \G(e)\AND q & \equiv \G(e\AND q)   & f \W (g\OR e)  & \equivEU (f \W g)\OR e  & f\R (g\AND u) & \equivEU (f \R g)\AND u & q \R\X f   & \equiv \X(q \R f)        \\
+  \X q        & \equiv q             & q \AND \X f    & \equivNeu \X(q \AND f)  & q\OR \X f     & \equivNeu \X(q \OR f)                                           \\
+              &                      & \X(q \AND f)   & \equivEU q \AND \X f    & \X(q \OR f)   & \equivEU q\OR \X f                                              \\
 \end{align*}
 
 \begin{align*}
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 21bcf09e2..ddb90c776 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -1682,8 +1682,19 @@ namespace spot
             if (a.is_universal() && bo.is(op::W))
               return recurse(formula::Or({a, b}));
 
+            // (q R Xf) = X(q R f)
+            // (q U Xf) = X(q U f)
+            if (a.is_eventual() && a.is_universal()
+                && bo.is(op::R, op::U) && b.is(op::X))
+              return recurse(formula::X(formula::binop(o, a, b[0])));
+
             // e₁ W e₂ = Ge₁ | e₂
             // u₁ M u₂ = Fu₁ & u₂
+            //
+            // The above formulas are actually true if e₁ and u₁ are
+            // unconstrained, however there are many cases were such a
+            // more generic reduction rule will actually produce more
+            // states once the resulting formula is translated.
             if (!opt_.reduce_size_strictly)
               {
                 if (bo.is(op::W) && a.is_eventual() && b.is_eventual())
diff --git a/tests/core/det.test b/tests/core/det.test
index 79c9dcded..112876710 100755
--- a/tests/core/det.test
+++ b/tests/core/det.test
@@ -36,7 +36,7 @@ cat >formulas <<'EOF'
 1,5,a M G(F!b | X!a)
 1,4,G!a R XFb
 1,4,XF(!a | GFb)
-1,6,GF!a U Xa
+1,5,X(GF!a U a)
 1,5,(a | G(a M !b)) W Fc
 1,6,Fa W Xb
 1,9,X(a R ((!b & F!c) M X!a))
diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test
index 43dec64ae..b14677585 100755
--- a/tests/core/reduccmp.test
+++ b/tests/core/reduccmp.test
@@ -192,7 +192,11 @@ GFa <=> GFb, F(G(Fa&Fb)|G(!a&!b))
 FGa | (GFa & GFb), F(Ga | (G(Fa & Fb)))
 
 Gb W a, Gb|a
+a W Fb, a W Fb
 Fb M Fa, Fa & Fb
+a M Gb, a M Gb
+GFa R Xf, X(GFa R f)
+GFa U Xf, X(GFa U f)
 
 a U (b | G(a) | c), a W (b | c)
 a U (G(a)), Ga
diff --git a/tests/core/satmin.test b/tests/core/satmin.test
index 564106186..69bff3b85 100755
--- a/tests/core/satmin.test
+++ b/tests/core/satmin.test
@@ -1140,8 +1140,8 @@ cat >expected <<'EOF'
 "!(X(F((!(p0)) | (G(F(p1))))))","15",3
 "!(X(F((!(p0)) | (G(F(p1))))))","16",3
 "!(X(F((!(p0)) | (G(F(p1))))))","17",3
-"(G((F(!(p0))) U (!(p0)))) U (X(p0))","1",6
-"(G((F(!(p0))) U (!(p0)))) U (X(p0))","2",6
+"(G((F(!(p0))) U (!(p0)))) U (X(p0))","1",5
+"(G((F(!(p0))) U (!(p0)))) U (X(p0))","2",5
 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","3",5
 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","4",5
 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","6",5
@@ -1156,22 +1156,22 @@ cat >expected <<'EOF'
 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","15",5
 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","16",5
 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","17",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","1",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","2",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","3",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","4",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","6",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","7",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","8",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","9",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","10",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","11",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","12",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","13",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","14",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","15",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","16",5
-"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","17",5
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","1",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","2",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","3",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","4",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","6",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","7",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","8",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","9",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","10",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","11",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","12",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","13",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","14",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","15",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","16",4
+"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","17",4
 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","1",4
 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","2",5
 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","3",4