diff --git a/theories/list.v b/theories/list.v
index 3b05646885b314c4a1891bca7d1e53617a03722a..13188cc8063ec754ea74b42b0adce66550d84c0c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2743,6 +2743,26 @@ Proof.
   rewrite <-(elem_of_nil x).
   apply Hl, elem_of_cons. by left.
 Qed.
+Lemma list_subseteq_cons x l1 l2 : l1 ⊆ l2 → x :: l1 ⊆ x :: l2 .
+Proof.
+  intros Hin y Hy%elem_of_cons.
+  destruct Hy as [-> | Hy]; [by left|]. right. by apply Hin.
+Qed.
+Lemma list_subseteq_cons_r x l1 l2 : l1 ⊆ l2 → l1 ⊆ x :: l2.
+Proof. intros Hin y Hy. right. by apply Hin. Qed.
+Lemma list_delete_subseteq i l : delete i l ⊆ l.
+Proof.
+  revert i. induction l as [|x l IHl]; intros i; [done|].
+  destruct i as [|i];
+    [by apply list_subseteq_cons_r|by apply list_subseteq_cons].
+Qed.
+Lemma 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_cons|by apply list_subseteq_cons_r].
+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.