diff --git a/theories/telescopes.v b/theories/telescopes.v
index 17b70cf6d075f4c706e2614408a5975af22e944b..1a704fb84f292aa742c340ae3c6971ba96aec4ea 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -185,3 +185,10 @@ Proof.
     + rewrite <-(IH p (λ a, Ψ (TargS p a))).
       intros [??]. eauto.
 Qed.
+
+(* Teach typeclass resolution how to make progress on these binders *)
+Typeclasses Opaque tforall texist.
+Hint Extern 1 (tforall _) =>
+  progress cbn [tforall tele_fold tele_bind tele_app] : typeclass_instances.
+Hint Extern 1 (texist _) =>
+  progress cbn [texist tele_fold tele_bind tele_app] : typeclass_instances.