diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 7ed96a5415b6635cae0fdd4ac9f9ff53aa8549bb..91ff03c03ea33513b335b9745fcb2e7c151cebea 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -818,9 +818,8 @@ Section map.
   Proof.
     induction X as [|x' X IH] using gmultiset_ind; intros Hinj.
     - multiset_solver.
-    - rewrite gmultiset_map_disj_union, !multiplicity_disj_union, IH; [|done].
-      destruct (bool_decide (x = x'));
-        rewrite gmultiset_map_singleton; multiset_solver.
+    - rewrite gmultiset_map_disj_union, gmultiset_map_singleton, !multiplicity_disj_union.
+      destruct (bool_decide (x = x')); multiset_solver.
   Qed.
 
   Lemma gmultiset_map_eq_iff f X Y :