diff --git a/proof-libs/fstar/core/Rand_core.fsti b/proof-libs/fstar/core/Rand_core.fsti
index 2dfc1cc25..4e607ba2d 100644
--- a/proof-libs/fstar/core/Rand_core.fsti
+++ b/proof-libs/fstar/core/Rand_core.fsti
@@ -8,10 +8,14 @@ class t_RngCore (t_Self: Type0) = {
 }
 
 class t_CryptoRng (t_Self: Type0) = {
+  [@@@FStar.Tactics.Typeclasses.tcinstance]
+  _super_core: t_RngCore t_Self;
   marker_trait: unit
 }
 
 class t_CryptoRngCore (t_Self: Type0) = {
+  [@@@FStar.Tactics.Typeclasses.tcinstance]
+  _super_crypto: t_CryptoRng t_Self;
   f_rngcore: t_Self -> t_Self
 }