diff --git a/tests/telescopes.v b/tests/telescopes.v
index d231e29188b5ea3d5da6f0ca130643a23559640e..416d29c8c4cf62c022bbd3934b4968d3e42f89d9 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -79,3 +79,12 @@ Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False
 assert_succeeds exact [tele_arg true; 0].
 assert_succeeds refine [tele_arg true; 0].
 Abort.
+
+(* Assert that telescopes are cumulatively universe polymorphic.
+   See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
+ *)
+Section Cumulativity.
+  Monomorphic Universes Quant local.
+  Monomorphic Constraint local < Quant.
+  Example cumul (t : tele@{local}) : tele@{Quant} := t.
+End Cumulativity.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 2378216ea18776b08f38b416d35a16500db3c278..33f44ad92b627728e4a0f0abe657ce3e2054c1f5 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -2,6 +2,7 @@ From stdpp Require Import base tactics.
 From stdpp Require Import options.
 
 Local Set Universe Polymorphism.
+Local Set Polymorphic Inductive Cumulativity.
 
 (** Without this flag, Coq minimizes some universes to [Set] when they
     should not be, e.g. in [texist_exist].