diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index ad8ae295b5e1d837a260b7b5749dea1bc68eb5da..d160868c16fd5cca0d9df0b9e6fe99fbe74f3d33 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -188,7 +188,7 @@ Section offerReg_rules.
         symmetry. apply agree_included.
         by apply to_agree_included.
       + rewrite lookup_singleton_ne; eauto.
-        by rewrite left_id. }
+        simpl. by case_match. }
     by rewrite Hfoo.
   Qed.