Test case for `TCSimpl`.

tests/typeclasses.ref

+"tc_simpl_test"
+     : string
+1 goal
+  
+  P : nat → Prop
+  y : nat
+  ============================
+  P (S (S (S (S (S (S y))))))

tests/typeclasses.v

-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