diff --git a/theories/typing/type.v b/theories/typing/type.v
index 004b4433c70545c2f394ed2f3fd29fd75ab9bd9b..823bed72138f39f859c5f35e9fbe275d6bcbf106 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -88,7 +88,7 @@ Section type.
     (n ≤ m)%nat → shr_locsE l n ⊆ shr_locsE l m.
   Proof.
     induction 1; first done.
-    rewrite ->IHle. rewrite -Nat.add_1_l [(_ + _)%nat]comm.  (* FIXME last rewrite is very slow. *)
+    rewrite ->IHle. rewrite -Nat.add_1_l [(_ + _)%nat]comm_L.
     rewrite shr_locsE_shift. set_solver+.
   Qed.