diff --git a/theories/mapset.v b/theories/mapset.v
index 7481faadb0cd883f9d560dbad8ccd633de1b34fb..20529a20d0f39d0e2e6c5259b776de7c6f607037 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -130,4 +130,8 @@ Proof.
 Qed.
 End mapset.
 
+(** [mapset_elem_of] internally contains an equality; make sure that tactics do
+not unfold it and try to unify [∈] against goals with [=]. *)
+Opaque mapset_elem_of.
+
 Arguments mapset_eq_dec : simpl never.