diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index 27b2621475..3790039c1c 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -289,7 +289,8 @@ Section S.
 
 End S.
 
-
+#[global]
+Hint Extern 2 (subrelation (eiff _) _) => progress cbn : typeclass_instances.
 
 (** Typical boolean formulae *)
 Definition eKind (k: kind) := if k then Prop else bool.