diff --git a/tests/telescopes.v b/tests/telescopes.v
index 416d29c8c4cf62c022bbd3934b4968d3e42f89d9..30027fb50e9ffd257f7fbcecc56e045edb17568c 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,6 +2,11 @@ From stdpp Require Import tactics telescopes.
 
 Local Unset Mangle Names. (* for stable goal printing *)
 
+(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
+Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
+  texist P ↔ ex P.
+Proof. by rewrite texist_exist. Qed.
+
 Section accessor.
 (* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
 Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
@@ -48,11 +53,6 @@ is essentially just a (dependent) product.
  *)
 Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
 
-(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
-Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
-  texist P ↔ ex P.
-Proof. by rewrite texist_exist. Qed.
-
 (** [tele_arg ..] notation tests.
     These tests mainly test type annotations and casts in the [tele_arg]
     notations.