diff --git a/src/Enum.ml b/src/Enum.ml
index ff65242b62fd50ae30ec4c001cc5b98968c5209a..8791e699ce77318e025969afa876e7c188d241bd 100644
--- a/src/Enum.ml
+++ b/src/Enum.ml
@@ -32,6 +32,10 @@ let sum (enum1 : 'a enum) (enum2 : 'a enum) : 'a enum =
 let ( ++ ) =
   sum
 
+let exists (xs : 'a list) (enum : 'a -> 'b enum) : 'b enum =
+  fun s ->
+    IFSeq.exists xs (fun x -> enum x s)
+
 (* [up i j] is the list of the integers of [i] included up to [j] included. *)
 
 let rec up i j =
diff --git a/src/Enum.mli b/src/Enum.mli
index 535fd5a06ed07700493eb0588fc51fecf85e5306..e873f4bb1234c185bfc32c8e1135cce93557076b 100644
--- a/src/Enum.mli
+++ b/src/Enum.mli
@@ -36,6 +36,11 @@ val pay: 'a enum -> 'a enum
 val sum    : 'a enum -> 'a enum -> 'a enum
 val ( ++ ) : 'a enum -> 'a enum -> 'a enum
 
+(* [exists xs e] is the union of all enumerations of the form [e x], where [x]
+   is drawn from the list [xs]. (This is an indexed sum.) It is up to the user
+   to ensure that the sets [e1] and [e2] are disjoint. *)
+val exists: 'a list -> ('a -> 'b enum) -> 'b enum
+
 (* [product e1 e2] is the Cartesian product of the enumerations
    [e1] and [e2]. *)
 val product: 'a enum -> 'b enum -> ('a * 'b) enum
diff --git a/src/IFSeq.ml b/src/IFSeq.ml
index ea721411d8ecdd916adce1d52b9d8cafb1a559e5..b8deaeaf10495be43ce9ff3cac31b506c5b0b463 100644
--- a/src/IFSeq.ml
+++ b/src/IFSeq.ml
@@ -8,6 +8,11 @@ include IFSeqSyn.Make(Z)
 let bigsum ss =
   List.fold_left sum zero ss
 
+(* Indexed iterated sum. *)
+
+let exists (xs : 'a list) (s : 'a -> 'b seq) : 'b seq =
+  bigsum (List.map s xs)
+
 (* Extract a randomly chosen sample of [m] elements out of a sequence [s]. *)
 
 (* We do not protect against repetitions, as they are unlikely when [s] is
diff --git a/src/IFSeq.mli b/src/IFSeq.mli
index 934d55f3c5a5f38e177e7e01d70eb68fb74c07fa..8300bbe74db09e04f69c9e6deb35316ac7e437e7 100644
--- a/src/IFSeq.mli
+++ b/src/IFSeq.mli
@@ -8,6 +8,9 @@ include IFSEQ with type index = Z.t
 (* Iterated sum. *)
 val bigsum: 'a seq list -> 'a seq
 
+(* Indexed iterated sum. *)
+val exists: 'a list -> ('a -> 'b seq) -> 'b seq
+
 (* [sample m s k] is an explicit sequence of at most [m] elements extracted
    out of the implicit sequence [s], prepended in front of the existing
    sequence [k]. If [length s] at most [m], then all elements of [s] are