diff --git a/theories/hocap/contrib_bag.v b/theories/hocap/contrib_bag.v
index 56573c38cf2eaf724bc93e0776285b9f7373553c..d0c6b779011b7c4d600880ac0abaf45363f31b77 100644
--- a/theories/hocap/contrib_bag.v
+++ b/theories/hocap/contrib_bag.v
@@ -76,11 +76,6 @@ Section proof.
     iNext. iExists _; iFrame.
   Qed.
 
-  Local Ltac multiset_solver :=
-    intro;
-    repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union);
-    (lia || naive_solver).
-
   Lemma popBag_spec γb γ x X :
     {{{ bagM γb γ x ∗ bagPart γ 1 X }}}
        popBag b x