diff --git a/stdpp/list.v b/stdpp/list.v
index 12db6e64352f540754b72d860d70af97521bd2c0..ac0f36208c4ff41d5cbd1d381b376dff3d737335 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -3651,6 +3651,18 @@ Proof.
 Qed.
 Lemma list_subseteq_cons x l1 l2 : l1 ⊆ l2 → l1 ⊆ x :: l2.
 Proof. intros Hin y Hy. right. by apply Hin. Qed.
+Lemma list_subseteq_app_l l1 l2 l : l1 ⊆ l2 → l1 ⊆ l2 ++ l.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
+Lemma list_subseteq_app_r l1 l2 l : l1 ⊆ l2 → l1 ⊆ l ++ l2.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
+
+Lemma list_app_subseteq l1 l2 l :
+  l1 ++ l2 ⊆ l ↔ l1 ⊆ l ∧ l2 ⊆ l.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_app. naive_solver. Qed.
+Lemma list_cons_subseteq x l1 l2 :
+  x :: l1 ⊆ l2 ↔ x ∈ l2 ∧ l1 ⊆ l2.
+Proof. unfold subseteq, list_subseteq. setoid_rewrite elem_of_cons. naive_solver. Qed.
+
 Lemma list_delete_subseteq i l : delete i l ⊆ l.
 Proof.
   revert i. induction l as [|x l IHl]; intros i; [done|].
@@ -3664,6 +3676,10 @@ Proof.
   destruct (decide (P x));
     [by apply list_subseteq_skip|by apply list_subseteq_cons].
 Qed.
+Lemma drop_subseteq n l : drop n l ⊆ l.
+Proof. rewrite <-(take_drop n l) at 2. apply list_subseteq_app_r. done. Qed.
+Lemma take_subseteq n l : take n l ⊆ l.
+Proof. rewrite <-(take_drop n l) at 2. apply list_subseteq_app_l. done. Qed.
 
 Global Instance list_subseteq_Permutation:
   Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .