diff --git a/CHANGELOG.md b/CHANGELOG.md
index 32d2f14cd8c367fb5987ebe5a0e5d3f0993e2dcf..ffa45da8ae030651063976988800c245d92c830e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,8 @@ API-breaking change is listed.
   `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
 - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
   `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add lemmas about `sublist_of`: `elem_of_sublist`, `sublist_NoDup`,
+  ` sublist_singleton_elem_of`. (by Kimaya Bedarkar)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/stdpp/list.v b/stdpp/list.v
index 4a96bd886bcf83bd1377c6f4ce4ced2b13e2387b..b2bfa9b46a79162a5156880f1a49c2edbae11f8b 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -2591,6 +2591,57 @@ Proof.
   rewrite (assoc_L (++)) in E; simplify_list_eq.
   eauto using sublist_inserts_r.
 Qed.
+Lemma elem_of_sublist (k : A) l1 l2 :
+  l1 `sublist_of` l2 →
+  k ∈ l1 →
+  k ∈ l2.
+Proof.
+  induction 1; try done.
+  - rewrite elem_of_cons.
+    intros [-> | Hin]; first by apply elem_of_list_here.
+    rewrite elem_of_cons.
+    right.
+    by apply IHsublist.
+  - rewrite elem_of_cons.
+    right.
+    by apply IHsublist.
+Qed.
+Lemma sublist_NoDup l1 l2:
+  NoDup l2 →
+  l1 `sublist_of` l2 →
+  NoDup l1.
+Proof.
+  intros Hnodup.
+  induction 1; try done.
+  - rewrite NoDup_cons in Hnodup.
+    destruct Hnodup as [Hnotin Hnodup].
+    rewrite NoDup_cons.
+    split; last by apply IHsublist.
+    intro Hin.
+    apply Hnotin.
+    by eapply elem_of_sublist.
+  - rewrite NoDup_cons in Hnodup.
+    destruct Hnodup as [Hnotin Hnodup].
+    by apply IHsublist.
+Qed.
+Lemma sublist_singleton_elem_of (k : A) (l : list A) :
+  [k] `sublist_of` l ↔ k ∈ l.
+Proof.
+  induction l as [| hd tail IH].
+  - by rewrite sublist_nil_r; rewrite elem_of_nil.
+  - split.
+    + inversion 1; first by apply elem_of_list_here.
+      subst.
+      rewrite elem_of_cons.
+      right.
+      by rewrite <-IH.
+    + inversion 1; subst.
+      * apply sublist_skip.
+        apply sublist_nil_l.
+      * apply sublist_cons.
+        by rewrite IH.
+Qed.
+
 Global Instance: PartialOrder (@sublist A).
 Proof.
   split; [split|].