diff --git a/stdpp/base.v b/stdpp/base.v
index 26fff8e206da17cb4a552bf1e09f482410e670c5..3488b6fd49046b5e7820613c47c5ff9ed5ae97e9 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1050,6 +1050,14 @@ Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
 Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope.
 Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
 
+Class CProd A B C := cprod : A → B → C.
+Global Hint Mode CProd ! ! - : typeclass_instances.
+Global Instance: Params (@cprod) 4 := {}.
+Infix "×" := cprod (at level 37, left associativity) : stdpp_scope.
+Notation "(×)" := cprod (only parsing) : stdpp_scope.
+Notation "( x ×.)" := (cprod x) (only parsing) : stdpp_scope.
+Notation "(.× x )" := (λ y, cprod y x) (only parsing) : stdpp_scope.
+
 Class Singleton A B := singleton: A → B.
 Global Hint Mode Singleton - ! : typeclass_instances.
 Global Instance: Params (@singleton) 3 := {}.
diff --git a/stdpp/boolset.v b/stdpp/boolset.v
index 5e1b5e1dd3e6fd1f79b2d4ebdfab4450d856fc5b..003deaaedac51fecb18eb73c8c5db2ecadea85a6 100644
--- a/stdpp/boolset.v
+++ b/stdpp/boolset.v
@@ -17,6 +17,10 @@ Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
 Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
+Global Instance boolset_cprod {A B} :
+  CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
+
 Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
 Proof.
   split; [split; [split| |]|].
@@ -31,6 +35,24 @@ Qed.
 Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
 
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ X1 × X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof.
+  destruct X1, X2.
+  unfold cprod, boolset_cprod, elem_of, boolset_elem_of.
+  cbn.
+  by rewrite andb_True.
+Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (sa : boolset A) (sb : boolset B) x P Q :
+  SetUnfoldElemOf x.1 sa P -> SetUnfoldElemOf x.2 sb Q ->
+  SetUnfoldElemOf x (sa × sb) (P ∧ Q).
+Proof using.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 sa P),
+    (set_unfold_elem_of x.2 sb Q).
+Qed.
+
 Global Typeclasses Opaque boolset_elem_of.
 Global Opaque boolset_empty boolset_singleton boolset_union
-  boolset_intersection boolset_difference.
+  boolset_intersection boolset_difference boolset_cprod.
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index dd093390f3057e82d7d0ea740ce0616a77cbd333..0152607f0e49656cbe5017cbbbb8329767dab29e 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -823,4 +823,31 @@ Section gset.
   Qed.
 End gset.
 
+Section gset_cprod.
+  Context `{Countable A}.
+  Context `{Countable B}.
+
+  #[global] Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) :=
+    λ sa sb, set_fold (fun e1 res => res ∪ set_map (e1,.) sb) ∅ sa.
+
+  Lemma elem_of_gset_cprod (sa : gset A) (sb : gset B) x :
+    x ∈ sa × sb ↔ x.1 ∈ sa ∧ x.2 ∈ sb.
+  Proof.
+    unfold cprod, gset_cprod.
+    destruct x.
+    apply (set_fold_ind_L (λ sab sa, ∀ a b, (a,b) ∈ sab ↔ a ∈ sa ∧ b ∈ sb)).
+    all: set_solver.
+  Qed.
+
+  Global Instance set_unfold_gset_cprod (sa : gset A) (sb : gset B) x (P : Prop) Q :
+    SetUnfoldElemOf x.1 sa P -> SetUnfoldElemOf x.2 sb Q ->
+    SetUnfoldElemOf x (sa × sb) (P ∧ Q).
+  Proof using.
+    intros ??; constructor.
+    by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 sa P),
+      (set_unfold_elem_of x.2 sb Q).
+  Qed.
+
+End gset_cprod.
+
 Global Typeclasses Opaque gset.
diff --git a/stdpp/list.v b/stdpp/list.v
index 9b25e6d9dc04d99d29a8c2dfb80b33fcca4e85bc..acf4f7b8fbf036ad96347fb55a88d38e78933670 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -68,6 +68,10 @@ Inductive list_equiv `{Equiv A} : Equiv (list A) :=
   | cons_equiv x y l k : x ≡ y → l ≡ k → x :: l ≡ y :: k.
 Global Existing Instance list_equiv.
 
+(** The operation [l × l'] gives the Cartesian product of both lists *)
+Global Instance list_cprod {A B} : CProd (list A) (list B) (list (A * B)) :=
+  @list_prod A B.
+
 (** The operation [l !! i] gives the [i]th element of the list [l], or [None]
 in case [i] is out of bounds. *)
 Global Instance list_lookup {A} : Lookup nat A (list A) :=
@@ -946,6 +950,14 @@ Proof.
   split; auto using elem_of_reverse_2.
   intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
 Qed.
+Lemma elem_of_list_cprod {B} l1 (l2 : list B) (x : A * B) :
+  x ∈ l1 × l2 ↔ x.1 ∈ l1 ∧ x.2 ∈ l2.
+Proof.
+  unfold cprod, list_cprod.
+  setoid_rewrite elem_of_list_In.
+  destruct x.
+  apply in_prod_iff.
+Qed.
 
 Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
 Proof.
diff --git a/stdpp/listset.v b/stdpp/listset.v
index 8961894dfe731c1c5ce99e0cf5194a61e7cb50e1..ad76367650e80711c07cdeb46ee634892dcc4f7d 100644
--- a/stdpp/listset.v
+++ b/stdpp/listset.v
@@ -47,6 +47,8 @@ Global Instance listset_intersection: Intersection (listset A) :=
   λ '(Listset l) '(Listset k), Listset (list_intersection l k).
 Global Instance listset_difference: Difference (listset A) :=
   λ '(Listset l) '(Listset k), Listset (list_difference l k).
+Global Instance listset_cprod {B}: CProd (listset A) (listset B) (listset (A * B)) :=
+  λ '(Listset l) '(Listset k), Listset (l × k).
 
 Local Instance listset_set: Set_ A (listset A).
 Proof.
@@ -83,3 +85,20 @@ Proof.
   - intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
     simpl. by rewrite elem_of_list_bind.
 Qed.
+
+Lemma elem_of_listset_cprod {A B} (X1 : listset A) (X2 : listset B) (x : A * B) :
+  x ∈ X1 × X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof.
+  destruct X1, X2.
+  unfold cprod, listset_cprod, elem_of, listset_elem_of.
+  by set_unfold.
+Qed.
+
+Global Instance set_unfold_listset_cprod {A B} (sa : listset A) (sb : listset B) x P Q :
+  SetUnfoldElemOf x.1 sa P -> SetUnfoldElemOf x.2 sb Q ->
+  SetUnfoldElemOf x (sa × sb) (P ∧ Q).
+Proof using.
+  intros ??; constructor.
+  by rewrite elem_of_listset_cprod, (set_unfold_elem_of x.1 sa P),
+    (set_unfold_elem_of x.2 sb Q).
+Qed.
diff --git a/stdpp/propset.v b/stdpp/propset.v
index 7a220edc8b008ad18e199a4d4c67c30375901bd4..1f6a60b81c20a8c7d70b4e02b6ddb86c190155e0 100644
--- a/stdpp/propset.v
+++ b/stdpp/propset.v
@@ -26,6 +26,9 @@ Global Instance propset_difference {A} : Difference (propset A) := λ X1 X2,
   {[ x | x ∈ X1 ∧ x ∉ X2 ]}.
 Global Instance propset_top_set {A} : TopSet A (propset A).
 Proof. split; [split; [split| |]|]; by repeat intro. Qed.
+Global Instance propset_cprod {A B} :
+  CProd (propset A) (propset B) (propset (A * B)) := λ X1 X2,
+    {[ x | x.1 ∈ X1 ∧ x.2 ∈ X2 ]}.
 
 Lemma elem_of_PropSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
 Proof. done. Qed.
@@ -52,6 +55,19 @@ Global Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
   SetUnfoldSimpl (P x) Q → SetUnfoldElemOf x (PropSet P) Q.
 Proof. intros HPQ. constructor. apply HPQ. Qed.
 
+Lemma elem_of_propset_cprod {A B} (X1 : propset A) (X2 : propset B) (x : A * B) :
+  x ∈ X1 × X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. unfold cprod, propset_cprod. by set_unfold. Qed.
+
+Global Instance set_unfold_propset_cprod {A B} (sa : propset A) (sb : propset B) x P Q :
+  SetUnfoldElemOf x.1 sa P -> SetUnfoldElemOf x.2 sb Q ->
+  SetUnfoldElemOf x (sa × sb) (P ∧ Q).
+Proof using.
+  intros ??; constructor.
+  by rewrite elem_of_propset_cprod, (set_unfold_elem_of x.1 sa P),
+    (set_unfold_elem_of x.2 sb Q).
+Qed.
+
 Global Opaque propset_elem_of propset_top propset_empty propset_singleton.
-Global Opaque propset_union propset_intersection propset_difference.
+Global Opaque propset_union propset_intersection propset_difference propset_cprod.
 Global Opaque propset_ret propset_bind propset_fmap propset_join.
diff --git a/stdpp/sets.v b/stdpp/sets.v
index a681d7c5d44cee30e62de36281636503d1b7060a..e4d8a62d1bcfd1c09af4e651f0b79ac897b904e2 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -287,6 +287,15 @@ Section set_unfold_list.
     intros ??; constructor.
     by rewrite elem_of_app, (set_unfold_elem_of x l P), (set_unfold_elem_of x k Q).
   Qed.
+  Global Instance set_unfold_list_cprod {B} (x : A * B) l (k : list B) P Q :
+    SetUnfoldElemOf x.1 l P → SetUnfoldElemOf x.2 k Q →
+    SetUnfoldElemOf x (l × k) (P ∧ Q).
+  Proof.
+    intros ??; constructor.
+    by rewrite elem_of_list_cprod, (set_unfold_elem_of x.1 l P),
+      (set_unfold_elem_of x.2 k Q).
+  Qed.
+
   Global Instance set_unfold_included l k (P Q : A → Prop) :
     (∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf x k (Q x)) →
     SetUnfold (l ⊆ k) (∀ x, P x → Q x).