diff --git a/src/core/tree.ml b/src/core/tree.ml
index 1e96ae00a..e94d8cbf7 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -240,7 +240,9 @@ module CM = struct
   (** Type of clause matrices. *)
   type t =
     { clauses   : clause list
-    (** The rules. *)
+    (** The rewrite rules. The order is significant when the {!Sequen}
+        strategy is used: the rewrite rules are ordered by decreasing
+        priority. *)
     ; slot      : int
     (** Index of next slot to use in [vars] array to store variables. *)
     ; positions : arg list
diff --git a/src/handle/command.ml b/src/handle/command.ml
index f99821097..25bb420bb 100644
--- a/src/handle/command.ml
+++ b/src/handle/command.ml
@@ -218,12 +218,17 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
     (* Scope rules, and check that they preserve typing. Return the list of
        rules [srs] and also a map [map] mapping every symbol defined by a rule
        of [srs] to its defining rules. *)
-      let handle_rule (srs, map) r =
+      let handle_rule r (srs, map) =
         let (s,r) as sr = check_rule ss r in
         let h = function Some rs -> Some(r::rs) | None -> Some[r] in
         sr::srs, SymMap.update s h map
       in
-      let srs, map = List.fold_left handle_rule ([], SymMap.empty) rs in
+      (* The order of rules must be kept between [rs] and [srs].
+         That is, the following assertion should hold
+         [assert (srs = List.map (check_rule ss) rs);] if we could compare
+         functional values. Failure to keep that invariant breaks some
+         evaluation strategies. *)
+      let srs, map = List.fold_right handle_rule rs ([], SymMap.empty) in
       (* /!\ Update decision trees without adding the rules themselves. It is
          important for local confluence checking. *)
       SymMap.iter Tree.update_dtree map;
diff --git a/tests/OK/1033.lp b/tests/OK/1033.lp
new file mode 100644
index 000000000..e2b4c5e82
--- /dev/null
+++ b/tests/OK/1033.lp
@@ -0,0 +1,9 @@
+// Test on the sequential reduction strategy
+constant symbol I: TYPE;
+constant symbol i: I;
+constant symbol j: I;
+sequential symbol k: I → I;
+rule k i ↪ i
+with k i ↪ j;
+
+assert ⊢ k i ≡ i;
diff --git a/tests/regressions/hrs.expected b/tests/regressions/hrs.expected
index f3dc68acd..9de812644 100644
--- a/tests/regressions/hrs.expected
+++ b/tests/regressions/hrs.expected
@@ -34,16 +34,16 @@ $10_0 : t
 (RULES
 A(L($x,$y),$z) -> $y($z),
 B($x,$z,$y) -> $y($z),
-A(A(tests_OK_boolean_bool_and,$1_0),tests_OK_boolean_false) -> tests_OK_boolean_false,
-A(A(tests_OK_boolean_bool_and,$2_0),tests_OK_boolean_true) -> $2_0,
-A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),$3_0) -> tests_OK_boolean_false,
-A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),$4_0) -> $4_0,
+A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),$1_0) -> $1_0,
+A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),$2_0) -> tests_OK_boolean_false,
+A(A(tests_OK_boolean_bool_and,$3_0),tests_OK_boolean_true) -> $3_0,
+A(A(tests_OK_boolean_bool_and,$4_0),tests_OK_boolean_false) -> tests_OK_boolean_false,
 tests_OK_boolean_bool_impl -> L(tests_OK_boolean_B,\82.L(tests_OK_boolean_B,\83.A(A(tests_OK_boolean_bool_or,83),A(tests_OK_boolean_bool_neg,82)))),
-A(tests_OK_boolean_bool_neg,tests_OK_boolean_false) -> tests_OK_boolean_true,
 A(tests_OK_boolean_bool_neg,tests_OK_boolean_true) -> tests_OK_boolean_false,
-A(A(tests_OK_boolean_bool_or,$7_0),tests_OK_boolean_false) -> $7_0,
-A(A(tests_OK_boolean_bool_or,$8_0),tests_OK_boolean_true) -> tests_OK_boolean_true,
-A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),$9_0) -> $9_0,
-A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),$10_0) -> tests_OK_boolean_true,
+A(tests_OK_boolean_bool_neg,tests_OK_boolean_false) -> tests_OK_boolean_true,
+A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),$7_0) -> tests_OK_boolean_true,
+A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),$8_0) -> $8_0,
+A(A(tests_OK_boolean_bool_or,$9_0),tests_OK_boolean_true) -> tests_OK_boolean_true,
+A(A(tests_OK_boolean_bool_or,$10_0),tests_OK_boolean_false) -> $10_0,
 tests_OK_boolean_bool_xor -> L(tests_OK_boolean_B,\84.L(tests_OK_boolean_B,\85.B(tests_OK_boolean_B,A(A(tests_OK_boolean_bool_and,84),A(tests_OK_boolean_bool_neg,85)),\86.B(tests_OK_boolean_B,A(A(tests_OK_boolean_bool_and,85),A(tests_OK_boolean_bool_neg,84)),\87.A(A(tests_OK_boolean_bool_or,86),87)))))
 )
diff --git a/tests/regressions/xtc.expected b/tests/regressions/xtc.expected
index 94f5c4035..7510feae8 100644
--- a/tests/regressions/xtc.expected
+++ b/tests/regressions/xtc.expected
@@ -5,34 +5,34 @@
     <rules>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>1_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>1_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.false</name></funapp>
+          <var>1_0</var>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>2_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>2_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <var>2_0</var>
+          <funapp><name>tests.OK.boolean.false</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>3_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>3_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.false</name></funapp>
+          <var>3_0</var>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>4_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>4_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <var>4_0</var>
+          <funapp><name>tests.OK.boolean.false</name></funapp>
         </rhs>
       </rule>
       <rule>
@@ -45,50 +45,50 @@
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.true</name></funapp>
+          <funapp><name>tests.OK.boolean.false</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.false</name></funapp>
+          <funapp><name>tests.OK.boolean.true</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>7_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>7_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <var>7_0</var>
+          <funapp><name>tests.OK.boolean.true</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>8_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>8_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.true</name></funapp>
+          <var>8_0</var>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>9_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>9_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <var>9_0</var>
+          <funapp><name>tests.OK.boolean.true</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>10_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>10_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.true</name></funapp>
+          <var>10_0</var>
         </rhs>
       </rule>
       <rule>