diff --git a/theories/list.v b/theories/list.v
index b78ba495a5ac39dcd8daa24743185c7de4e1a556..965096f52f202d657518168b34007da1d852bb26 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -987,6 +987,13 @@ Proof.
   intros; eapply elem_of_list_lookup_2.
   destruct (nth_lookup_or_length l i d); [done | by lia].
 Qed.
+Lemma elem_of_list_delete x i l :
+  x ∈ delete i l → x ∈ l.
+Proof.
+  revert i. induction l as [|z l IHl]; [done|]; intros i Hin.
+  destruct i as [|i]; [by right|]. apply elem_of_cons in Hin.
+  destruct Hin as [-> | Hin]; [by left|]. right. by eapply IHl.
+Qed.
 
 Lemma not_elem_of_app_cons_inv_l x y l1 l2 k1 k2 :
   x ∉ k1 → y ∉ l1 →
@@ -2418,6 +2425,18 @@ Proof.
     auto using sublist_inserts_l, sublist_skip.
   - intros (?&?&?&?&?); subst. auto using sublist_app.
 Qed.
+Lemma sublist_app_cons_inv l1 l2 l x :
+  l1 ++ x :: l2 `sublist_of` l →
+  ∃ l1' l2', l = l1' ++ x :: l2' ∧ l1 `sublist_of` l1' ∧ l2 `sublist_of` l2'.
+Proof.
+  intros Hl.
+  apply sublist_app_l in Hl as (k1&k2&->&Hle1&Hle2).
+  apply sublist_cons_l in Hle2 as (k1'&k2'&->&Hle3).
+  exists (k1++k1'), k2'.
+  split; [by rewrite app_assoc|]. split; [|done].
+  apply sublist_app_r. exists l1, [].
+  split; [by rewrite app_nil_r|]. split; [done|apply sublist_nil_l].
+Qed.
 Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist_of` k ++ l2 → l1 `sublist_of` l2.
 Proof.
   induction k as [|y k IH]; simpl; [done |].
@@ -2473,6 +2492,21 @@ Proof.
   - destruct (IH k) as [is His]. exists (is ++ [length k]).
     rewrite fold_right_app. simpl. by rewrite delete_middle.
 Qed.
+Lemma sublist_le l1 l2 :
+  l1 `sublist_of` l2 → l1 ⊆ l2.
+Proof.
+  intros Hle%sublist_alt x Hin. destruct Hle as [l' ->].
+  induction l' as [|y l' IHl']; [done|]. by eapply IHl', elem_of_list_delete.
+Qed.
+Lemma elem_of_sublist x l1 l2 :
+  x ∈ l1 → l1 `sublist_of` l2 → x ∈ l2.
+Proof. intros Hin Hle. by apply (sublist_le l1 l2 Hle). Qed.
+Lemma filter_sublist P `{! ∀ x : A, Decision (P x)} l :
+  filter P l `sublist_of` l.
+Proof.
+  induction l as [|x l IHl]; [done|]. rewrite filter_cons.
+  by destruct (decide (P x)); [apply sublist_skip|apply sublist_cons].
+Qed.
 Lemma Permutation_sublist l1 l2 l3 :
   l1 ≡ₚ l2 → l2 `sublist_of` l3 → ∃ l4, l1 `sublist_of` l4 ∧ l4 ≡ₚ l3.
 Proof.
@@ -2817,11 +2851,7 @@ Proof.
 Qed.
 Lemma list_filter_subseteq P `{!∀ x : A, Decision (P x)} l :
   filter P l ⊆ l.
-Proof.
-  induction l as [|x l IHl]; [done|]. rewrite filter_cons.
-  destruct (decide (P x));
-    [by apply list_subseteq_skip|by apply list_subseteq_cons].
-Qed.
+Proof. apply sublist_le, filter_sublist. Qed.
 
 Global Instance list_subseteq_Permutation: Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
 Proof. intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk. Qed.