diff --git a/theories/listset.v b/theories/listset.v
index 23ac7c389a7780175bd6a1344908f5e3e80721a2..0d864ce8f584415ec0d022a9856bd0ecd92dc480 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -38,7 +38,12 @@ Proof.
   abstract (by rewrite listset_empty_alt).
 Defined.
 
-Context `{!EqDecision A}.
+Context `{Aeq : !EqDecision A}.
+
+Global Instance listset_elem_of_dec : RelDecision (∈@{listset A}).
+Proof using Aeq.
+  refine (λ x X, cast_if (decide (x ∈ listset_car X))); done.
+Defined.
 
 Global Instance listset_intersection: Intersection (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_intersection l' k').