diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 3d164a8e8394e9075b4409ad8ce0a2a9e0e643bb..c71848299ef978d2b7cd60151d7bc419edd84786 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -204,18 +204,18 @@ Section multiset_unfold.
 
   Global Instance set_unfold_multiset_equiv X Y f g :
     (∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
-    SetUnfold (X ≡ Y) (∀ x, f x = g x).
+    SetUnfold (X ≡ Y) (∀ x, f x = g x) | 0.
   Proof.
     constructor. apply forall_proper; intros x.
     by rewrite (multiset_unfold x X (f x)), (multiset_unfold x Y (g x)).
   Qed.
   Global Instance set_unfold_multiset_eq X Y f g :
     (∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
-    SetUnfold (X = Y) (∀ x, f x = g x).
+    SetUnfold (X = Y) (∀ x, f x = g x) | 0.
   Proof. constructor. unfold_leibniz. by apply set_unfold_multiset_equiv. Qed.
   Global Instance set_unfold_multiset_subseteq X Y f g :
     (∀ x, MultisetUnfold x X (f x)) → (∀ x, MultisetUnfold x Y (g x)) →
-    SetUnfold (X ⊆ Y) (∀ x, f x ≤ g x).
+    SetUnfold (X ⊆ Y) (∀ x, f x ≤ g x) | 0.
   Proof.
     constructor. apply forall_proper; intros x.
     by rewrite (multiset_unfold x X (f x)), (multiset_unfold x Y (g x)).