From 5030bc10c47f93999c152e3aaf2fe473ee6bff21 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 10:50:34 +0000
Subject: [PATCH] improve proof

---
 theories/list.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index d568974e..9a52d687 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.
-- 
GitLab