diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index 52963ddaf086b2eed0242f48382d184ba493b68b..2c58e6389dcd6063da7a3f15a26d2863bc62b4f6 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -20,6 +20,3 @@
   γ1 x ∨ γ2 x
 [TEST x y : nat, x = y]
      : Prop
-tele_arg@{Top.70}
-     : tele@{Top.70} → Type@{Top.70}
-(* {Top.70} |=  *)
diff --git a/tests/telescopes.v b/tests/telescopes.v
index a24a122fe914639e61733a6f0a9585144b382368..22b3b92f314d45dde8189e45c4c1c6233c10d585 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -42,13 +42,8 @@ Notation "'[TEST'  x .. z ,  P ']'" :=
   (x binder, z binder).
 Check [TEST (x y : nat), x = y].
 
-Local Set Printing Universes.
-Check tele_arg.
-Local Unset Printing Universes.
-
 (* [tele_arg t] should live at the same universe
    as the types inside of [t] because [tele_arg t]
    is essentially just a (dependent) product.
  *)
-Definition no_bump@{u} (t : tele@{u}) : tele@{u} :=
-  TeleS (fun _ : tele_arg@{u} t => TeleO).
+Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index b7410fb218cb2205c7d8d94031e22aa74fe7d3d4..e81d100c393ecffc6310dcbae9deb6ec23b28e03 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -53,7 +53,7 @@ Fixpoint tele_arg@{u} (t : tele@{u}) : Type@{u} :=
   end.
 Global Arguments tele_arg _ : simpl never.
 Notation TargO := tt (only parsing).
-Notation TargS a b := (@TeleArgCons _ (fun x => tele_arg (_ x)) a b) (only parsing).
+Notation TargS a b := (@TeleArgCons _ (fun x => tele_arg _) a b) (only parsing).
 Coercion tele_arg : tele >-> Sortclass.
 
 Fixpoint tele_app {TT : tele} {U} : (TT -t> U) -> TT → U :=
@@ -76,14 +76,14 @@ Local Coercion tele_app : tele_fun >-> Funclass.
  *)
 Lemma tele_arg_inv@{u+} {TT : tele@{u}} (a : tele_arg@{u} TT) :
   match TT as TT return tele_arg@{u} TT → Prop with
-  | TeleO => λ a, a = tt
-  | @TeleS t f => λ a, ∃ x a', a = {| tele_arg_head := x ; tele_arg_tail := a' |}
+  | TeleO => λ a, a = TargO
+  | @TeleS t f => λ a, ∃ x a', a = TargS x a'
   end a.
 Proof. destruct TT; destruct a; eauto. Qed.
 Lemma tele_arg_O_inv (a : TeleO) : a = ().
 Proof. exact (tele_arg_inv a). Qed.
 Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
-  ∃ x a', a = {| tele_arg_head := x ; tele_arg_tail := a' |}.
+  ∃ x a', a = TargS x a'.
 Proof. exact (tele_arg_inv a). Qed.
 
 (** Map below a tele_fun *)
@@ -115,7 +115,7 @@ Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
   match TT as TT return (TT → U) → TT -t> U with
   | TeleO => λ F, F tt
   | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
-      tele_bind (λ a, F {| tele_arg_head := x ; tele_arg_tail := a |})
+      tele_bind (λ a, F (TargS x a))
   end.
 Global Arguments tele_bind {_ !_} _ /.