diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 7684d7d40838464060f30fb8b40ce3366d4707e3..acb7334b9d649a36b102d8c6eae1c1eeb772f6fd 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -161,8 +161,7 @@ Section offerReg_rules.
         symmetry. apply agree_included.
         by apply to_agree_included.
       + rewrite lookup_singleton_ne; eauto.
-        destruct ((offerize <$> N !! i)) as [?|] eqn:He;
-          rewrite He; simpl; done. }
+        by case: ((offerize <$> N !! i)). }
     by rewrite Hfoo.
   Qed.