Forward compatibility patch for stdpp!555

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.