diff --git a/theories/list.v b/theories/list.v
index d568974efdd1b386250e73d3fb08f2a6b15e099e..9a52d6879d9b9907b534f928a3e1e97099242793 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2609,9 +2609,8 @@ Proof.
   split.
   - intros Hsub. eapply elem_of_submseteq; [|done].
     apply elem_of_list_singleton. done.
-  - intros [i Hlook]%elem_of_list_lookup.
-    eapply take_drop_middle in Hlook; rewrite <-Hlook.
-    eapply submseteq_cons_middle, submseteq_nil_l.
+  - intros (l1&l2&->)%elem_of_list_split.
+    apply submseteq_cons_middle, submseteq_nil_l.
 Qed.
 Lemma singleton_submseteq x y :
   [x] ⊆+ [y] ↔ x = y.