diff --git a/tests/typeclasses.ref b/tests/typeclasses.ref
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..55c62f13d8c3b7c6bf36088e49aa13bad99c688f 100644
--- a/tests/typeclasses.ref
+++ b/tests/typeclasses.ref
@@ -0,0 +1,8 @@
+"tc_simpl_test"
+     : string
+1 goal
+  
+  P : nat → Prop
+  y : nat
+  ============================
+  P (S (S (S (S (S (S y))))))
diff --git a/tests/typeclasses.v b/tests/typeclasses.v
index 899518d58e83d8427e42fb3ce1a0196fbaa24c74..500bf04664373a828f4bc124102bafb6391db20b 100644
--- a/tests/typeclasses.v
+++ b/tests/typeclasses.v
@@ -1,4 +1,16 @@
-From stdpp Require Import prelude.
+From stdpp Require Import strings.
+
+Lemma tc_simpl_test_lemma (P : nat → Prop) x y :
+  TCSimpl x y →
+  P x → P y.
+Proof. by intros ->%TCSimpl_eq. Qed.
+
+Check "tc_simpl_test".
+Lemma tc_simpl_test (P : nat → Prop) y : P (5 + S y).
+Proof.
+  apply (tc_simpl_test_lemma _ _ _ _). (* would be nicer with ssr [apply:] *)
+  Show.
+Abort.
 
 (** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
     Really, we want to set [Hint Mode Reflexive] in a way that this fails, but