diff --git a/theories/collections.v b/theories/collections.v
index bf72aa636e92da0b27c21d48633bcee648cace04..e0d70b8d77f6b29f66d41c01970d77bb82ef74a8 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -324,6 +324,10 @@ Section list_unfold.
     intros ??; constructor.
     by rewrite elem_of_app, (set_unfold (x ∈ l) P), (set_unfold (x ∈ k) Q).
   Qed.
+  Global Instance set_unfold_included l k (P Q : A → Prop) :
+    (∀ x, SetUnfold (x ∈ l) (P x)) → (∀ x, SetUnfold (x ∈ k) (Q x)) →
+    SetUnfold (l `included` k) (∀ x, P x → Q x).
+  Proof. by constructor; unfold included; set_unfold. Qed.
 End list_unfold.
 
 (** * Guard *)
diff --git a/theories/list.v b/theories/list.v
index 7dcf11c6cc76f21940c5e047746ba274f7398c73..36be6e46faa42b96cced5acb2134c0b7c8828e9c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -282,6 +282,9 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
      P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k').
 
 (** Set operations on lists *)
+Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2.
+Infix "`included`" := included (at level 70) : C_scope.
+
 Section list_set.
   Context {A} {dec : ∀ x y : A, Decision (x = y)}.
   Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)}
@@ -2017,6 +2020,12 @@ Section contains_dec.
     abstract (rewrite Permutation_alt; tauto).
   Defined.
 End contains_dec.
+
+(** ** Properties of [included] *)
+Global Instance included_preorder : PreOrder (@included A).
+Proof. split; firstorder. Qed.
+Lemma included_nil l : [] `included` l.
+Proof. intros x. by rewrite elem_of_nil. Qed.
 End more_general_properties.
 
 (** ** Properties of the [Forall] and [Exists] predicate *)