diff --git a/theories/list.v b/theories/list.v
index 568cfc867be04eab929b753e97b120a2645227f7..d568974efdd1b386250e73d3fb08f2a6b15e099e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2603,7 +2603,7 @@ Proof.
   by apply submseteq_skip, (submseteq_app_inv_l _ _ [x]).
 Qed.
 
-Lemma submseteq_singleton l x :
+Lemma singleton_submseteq_l l x :
   [x] ⊆+ l ↔ x ∈ l.
 Proof.
   split.
@@ -2613,6 +2613,9 @@ Proof.
     eapply take_drop_middle in Hlook; rewrite <-Hlook.
     eapply submseteq_cons_middle, submseteq_nil_l.
 Qed.
+Lemma singleton_submseteq x y :
+  [x] ⊆+ [y] ↔ x = y.
+Proof. rewrite singleton_submseteq_l. apply elem_of_list_singleton. Qed.
 
 Section submseteq_dec.
   Context `{!EqDecision A}.