diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index afac10f0b0fddd77cc435c1097c467da2a88d1fb..2c58e6389dcd6063da7a3f15a26d2863bc62b4f6 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -18,3 +18,5 @@
   Hγ : γ1 x
   ============================
   γ1 x ∨ γ2 x
+[TEST x y : nat, x = y]
+     : Prop
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 56633586fa2e6089fa9e591c61b2a8f505e48c4f..260b7283cbcda1dc77a908295c7d6e939293adf9 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -31,3 +31,13 @@ Proof.
 Qed.
 End tests.
 End accessor.
+
+(* Type inference for tele_app-based notation.
+(Relies on [&] bidirectionality hint of tele_app.) *)
+Definition test {TT : tele} (t : TT → Prop) : Prop :=
+  ∀.. x, t x ∧ t x.
+Notation "'[TEST'  x .. z ,  P ']'" :=
+  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+        (tele_app (λ x, .. (λ z, P) ..)))
+  (x binder, z binder).
+Check [TEST (x y : nat), x = y].