diff --git a/src/tool/sr.ml b/src/tool/sr.ml
index 1aefa6e18..0107eac62 100644
--- a/src/tool/sr.ml
+++ b/src/tool/sr.ml
@@ -122,8 +122,11 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
   if not (Unif.solve_noexn ~type_check:false p) then
     fatal pos "The LHS is not typable.";
   (* Try to simplify constraints. *)
-  let norm_constr (c,t,u) = (c, Eval.snf [] t, Eval.snf [] u) in
-  let lhs_constrs = List.map norm_constr !p.unsolved in
+  let norm_constr (c,t,u) =
+    (c, Eval.snf [] (cleanup t), Eval.snf [] (cleanup u)) in
+  let lhs_constrs =
+    List.filter (fun (_,t,u) -> Term.cmp t u <> 0)
+      (List.map norm_constr !p.unsolved) in
   if Logger.log_enabled () then
     log_subj "@[<v>LHS type: %a@ LHS constraints: %a@ rule: %a ↪ %a@]"
       term ty_lhs constrs lhs_constrs
@@ -207,7 +210,9 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
   (* Solving the typing constraints of the RHS. *)
   if not (Unif.solve_noexn p) then
     fatal pos "The rewriting rule does not preserve typing.";
-  let rhs_constrs = List.map norm_constr !p.unsolved in
+  let rhs_constrs =
+    List.filter (fun (_,t,u) -> Term.cmp t u <> 0)
+      (List.map norm_constr !p.unsolved) in
   (* [matches p t] says if [t] is an instance of [p]. *)
   let matches p t =
     let rec matches s l =
diff --git a/tests/OK/ind_AC.lp b/tests/OK/ind_AC.lp
new file mode 100644
index 000000000..ce05d1d6e
--- /dev/null
+++ b/tests/OK/ind_AC.lp
@@ -0,0 +1,25 @@
+symbol Prop : TYPE;
+injective symbol π: Prop → TYPE;
+builtin "Prop" ≔ Prop;
+builtin "P" ≔ π;
+
+symbol context: TYPE;
+symbol □ : context;
+associative commutative symbol ∙ : context → context → context;
+
+notation ∙ infix right 1;
+
+symbol γ: Prop → context;
+rule □ ∙  $H ↪ $H;
+
+inductive valid1: context → TYPE ≔
+| R1 h1 h2 : valid1 (h1 ∙ h2) → valid1 h2;
+
+inductive valid2: context → TYPE ≔
+| R2 h1 h2 : valid2 (h1 ∙ h2) → valid2 h1;
+
+inductive valid3: context → TYPE ≔
+| R3 p h : valid3 (h ∙ γ p) → valid3 h;
+
+inductive valid4: context → TYPE ≔
+| R4 p h : valid4 (γ p ∙ h) → valid4 h;
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index 2ba93dfe8..cd14ca0ac 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -51,7 +51,7 @@ do
         # "as"
         729);;
         # "notation"
-        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|991|706|1101|1190b|1190c|1120|1247|decimal);;
+        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|991|706|1101|1190b|1190c|1120|1247|decimal|ind_AC);;
         # "quantifier"
         683|650|573|565|430);;
         # nested module name