diff --git a/theories/listset.v b/theories/listset.v
index 5c3df887ace11d4f7e482ae0a985fa5160f7dd3e..1f318c7bf5d4296e075df712ea2ecbbe972b3fde 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -24,6 +24,16 @@ Proof.
   * by apply elem_of_list_singleton.
   * intros [?] [?]. apply elem_of_app.
 Qed.
+Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
+Proof.
+  destruct X as [l]; split; [|by intros; simplify_equality'].
+  intros [Hl _]; destruct l as [|x l]; [done|]. feed inversion (Hl x); left.
+Qed. 
+Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
+Proof.
+ refine (cast_if (decide (listset_car X = [])));
+  abstract (by rewrite listset_empty_alt).
+Defined.
 
 Context `{∀ x y : A, Decision (x = y)}.